/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 257

Reference: erdosproblems.com/257

namespace Erdos257

Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_257 : answer(sorry) (A : Set ), A.Infinite Irrational (∑' n : A, (1 : ) / (2 ^ n.1 - 1)) := True (A : Set ), A.Infinite Irrational (∑' (n : A), 1 / (2 ^ n - 1)) All goals completed! 🐙

Show that $$ \sum_{n} \frac{1}{2^n - 1} = \sum_{n} \frac{d(n)}{2^n}, $$ where $d(n)$ is the number of divisors of $n$.

@[category textbook, AMS 11] theorem erdos_257.variants.tsum_top_eq : ∑' n, 1 / (2 ^ n - 1 : ) = ∑' n, n.divisors.card / (2 ^ n : ) := ∑' (n : ), 1 / (2 ^ n - 1) = ∑' (n : ), n.divisors.card / 2 ^ n have hr : (1 / 2 : ) < 1 := ∑' (n : ), 1 / (2 ^ n - 1) = ∑' (n : ), n.divisors.card / 2 ^ n All goals completed! 🐙 -- The key Lambert-series identity from Mathlib (`k = 0`): -- `∑' n:ℕ+, (1/2)^n / (1 - (1/2)^n) = ∑' n:ℕ+, σ 0 n * (1/2)^n`, with summands rewritten. hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))key:∑' (n : ℕ+), n ^ 0 * (1 / 2) ^ n / (1 - (1 / 2) ^ n) = ∑' (n : ℕ+), ((ArithmeticFunction.sigma 0) n) * (1 / 2) ^ n := tsum_pow_div_one_sub_eq_tsum_sigma hr 0∑' (n : ), 1 / (2 ^ n - 1) = ∑' (n : ), n.divisors.card / 2 ^ n have hpos : n : , 0 < n (2 : ) 2 ^ n := fun n hn hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))key:∑' (n : ℕ+), n ^ 0 * (1 / 2) ^ n / (1 - (1 / 2) ^ n) = ∑' (n : ℕ+), ((ArithmeticFunction.sigma 0) n) * (1 / 2) ^ n := tsum_pow_div_one_sub_eq_tsum_sigma hr 0n:hn:0 < n2 2 ^ n simpa using pow_le_pow_right₀ (hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))key:∑' (n : ℕ+), n ^ 0 * (1 / 2) ^ n / (1 - (1 / 2) ^ n) = ∑' (n : ℕ+), ((ArithmeticFunction.sigma 0) n) * (1 / 2) ^ n := tsum_pow_div_one_sub_eq_tsum_sigma hr 0n:hn:0 < n1 2 All goals completed! 🐙 : (1 : ) 2) hn hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ n∑' (n : ), 1 / (2 ^ n - 1) = ∑' (n : ), n.divisors.card / 2 ^ n -- Domination by geometric series gives `ℕ`-summability of both sides. have hsummL : Summable fun n : 1 / (2 ^ n - 1 : ) := .of_nonneg_of_le (fun n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:0 1 / (2 ^ n - 1) hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:this:1 2 ^ n := one_le_pow₀ one_le_two0 1 / (2 ^ n - 1); hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:this:1 2 ^ n := one_le_pow₀ one_le_two0 1hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:this:1 2 ^ n := one_le_pow₀ one_le_two0 2 ^ n - 1 hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:this:1 2 ^ n := one_le_pow₀ one_le_two0 1hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:this:1 2 ^ n := one_le_pow₀ one_le_two0 2 ^ n - 1 All goals completed! 🐙) (fun n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:1 / (2 ^ n - 1) 2 * (1 / 2) ^ n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:h:n = 01 / (2 ^ n - 1) 2 * (1 / 2) ^ nhr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:h:n > 01 / (2 ^ n - 1) 2 * (1 / 2) ^ n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:h:n = 01 / (2 ^ n - 1) 2 * (1 / 2) ^ n All goals completed! 🐙 hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:h:n > 01 / (2 ^ n - 1) 2 * (1 / 2) ^ n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:h:n > 0h2:2 2 ^ n := hpos n h1 / (2 ^ n - 1) 2 * (1 / 2) ^ n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nn:h:n > 0h2:2 2 ^ n := hpos n h1 * 2 ^ n 2 * (2 ^ n - 1); All goals completed! 🐙) ((summable_geometric_of_norm_lt_one hr).mul_left 2) have hsummR : Summable fun n : (n.divisors.card : ) / (2 ^ n : ) := .of_nonneg_of_le (fun n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nhsummL:Summable fun n => 1 / (2 ^ n - 1) := Summable.of_nonneg_of_le (fun n => have this := one_le_pow₀ one_le_two; div_nonneg (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le this) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))) (fun n => Or.casesOn (Nat.eq_zero_or_pos n) (fun h => of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrArg (HDiv.hDiv 1) (Eq.trans (congrArg (fun x => x - 1) (Eq.trans (congrArg (HPow.hPow 2) h) (pow_zero 2))) (sub_self 1))) (div_zero 1))) (Eq.trans (congrArg (HMul.hMul 2) (Eq.trans (congr (congrArg HPow.hPow (one_div 2)) h) (pow_zero 2⁻¹))) (mul_one 2))) (Nat.ofNat_nonneg._simp_1 2))) fun h => have h2 := hpos n h; Eq.mpr (id (congrArg (fun _a => 1 / (2 ^ n - 1) _a) (have this := Eq.mpr (id (congrArg (fun _a => 2 * _a = 2 / 2 ^ n) (div_pow 1 2 n))) (Eq.mpr (id (congrArg (fun _a => 2 * (_a / 2 ^ n) = 2 / 2 ^ n) (one_pow n))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))))); this))) (Eq.mpr (id (congrArg (fun _a => _a) (propext (div_le_div_iff₀ (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Eq.refl (Int.ofNat 1))))) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n))))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))))) (Summable.mul_left 2 (summable_geometric_of_norm_lt_one hr))n:0 n.divisors.card / 2 ^ n All goals completed! 🐙) (fun n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nhsummL:Summable fun n => 1 / (2 ^ n - 1) := Summable.of_nonneg_of_le (fun n => have this := one_le_pow₀ one_le_two; div_nonneg (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le this) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))) (fun n => Or.casesOn (Nat.eq_zero_or_pos n) (fun h => of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrArg (HDiv.hDiv 1) (Eq.trans (congrArg (fun x => x - 1) (Eq.trans (congrArg (HPow.hPow 2) h) (pow_zero 2))) (sub_self 1))) (div_zero 1))) (Eq.trans (congrArg (HMul.hMul 2) (Eq.trans (congr (congrArg HPow.hPow (one_div 2)) h) (pow_zero 2⁻¹))) (mul_one 2))) (Nat.ofNat_nonneg._simp_1 2))) fun h => have h2 := hpos n h; Eq.mpr (id (congrArg (fun _a => 1 / (2 ^ n - 1) _a) (have this := Eq.mpr (id (congrArg (fun _a => 2 * _a = 2 / 2 ^ n) (div_pow 1 2 n))) (Eq.mpr (id (congrArg (fun _a => 2 * (_a / 2 ^ n) = 2 / 2 ^ n) (one_pow n))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))))); this))) (Eq.mpr (id (congrArg (fun _a => _a) (propext (div_le_div_iff₀ (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Eq.refl (Int.ofNat 1))))) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n))))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))))) (Summable.mul_left 2 (summable_geometric_of_norm_lt_one hr))n:n.divisors.card / 2 ^ n n ^ 1 * (1 / 2) ^ n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nhsummL:Summable fun n => 1 / (2 ^ n - 1) := Summable.of_nonneg_of_le (fun n => have this := one_le_pow₀ one_le_two; div_nonneg (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le this) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))) (fun n => Or.casesOn (Nat.eq_zero_or_pos n) (fun h => of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrArg (HDiv.hDiv 1) (Eq.trans (congrArg (fun x => x - 1) (Eq.trans (congrArg (HPow.hPow 2) h) (pow_zero 2))) (sub_self 1))) (div_zero 1))) (Eq.trans (congrArg (HMul.hMul 2) (Eq.trans (congr (congrArg HPow.hPow (one_div 2)) h) (pow_zero 2⁻¹))) (mul_one 2))) (Nat.ofNat_nonneg._simp_1 2))) fun h => have h2 := hpos n h; Eq.mpr (id (congrArg (fun _a => 1 / (2 ^ n - 1) _a) (have this := Eq.mpr (id (congrArg (fun _a => 2 * _a = 2 / 2 ^ n) (div_pow 1 2 n))) (Eq.mpr (id (congrArg (fun _a => 2 * (_a / 2 ^ n) = 2 / 2 ^ n) (one_pow n))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))))); this))) (Eq.mpr (id (congrArg (fun _a => _a) (propext (div_le_div_iff₀ (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Eq.refl (Int.ofNat 1))))) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n))))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))))) (Summable.mul_left 2 (summable_geometric_of_norm_lt_one hr))n:n.divisors.card / 2 ^ n n / 2 ^ n hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nhsummL:Summable fun n => 1 / (2 ^ n - 1) := Summable.of_nonneg_of_le (fun n => have this := one_le_pow₀ one_le_two; div_nonneg (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le this) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))) (fun n => Or.casesOn (Nat.eq_zero_or_pos n) (fun h => of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrArg (HDiv.hDiv 1) (Eq.trans (congrArg (fun x => x - 1) (Eq.trans (congrArg (HPow.hPow 2) h) (pow_zero 2))) (sub_self 1))) (div_zero 1))) (Eq.trans (congrArg (HMul.hMul 2) (Eq.trans (congr (congrArg HPow.hPow (one_div 2)) h) (pow_zero 2⁻¹))) (mul_one 2))) (Nat.ofNat_nonneg._simp_1 2))) fun h => have h2 := hpos n h; Eq.mpr (id (congrArg (fun _a => 1 / (2 ^ n - 1) _a) (have this := Eq.mpr (id (congrArg (fun _a => 2 * _a = 2 / 2 ^ n) (div_pow 1 2 n))) (Eq.mpr (id (congrArg (fun _a => 2 * (_a / 2 ^ n) = 2 / 2 ^ n) (one_pow n))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))))); this))) (Eq.mpr (id (congrArg (fun _a => _a) (propext (div_le_div_iff₀ (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Eq.refl (Int.ofNat 1))))) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n))))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))))) (Summable.mul_left 2 (summable_geometric_of_norm_lt_one hr))n:n.divisors.card n; All goals completed! 🐙) (summable_pow_mul_geometric_of_norm_lt_one 1 hr) -- Bridge `ℕ+` to `ℕ`: the `n = 0` term is `0` on both sides. hr:1 / 2 < 1 := of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x < 1) (Eq.trans (Eq.trans (congrArg norm (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) (Eq.refl (Nat.mul 1 1)) (Eq.refl 2))) Nat.cast_one (Eq.refl 2))) (norm_div 1 2)) (Eq.trans (Eq.trans (congr (congrArg HDiv.hDiv (CStarRing.norm_of_mem_unitary (of_eq_true (Eq.trans (Eq.trans (congrArg (Membership.mem (unitary )) (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) Nat.cast_one)) (OneMemClass.one_mem._simp_1 (unitary ))) (eq_true True.intro))))) (Real.norm_ofNat 2)) (one_div 2)) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)))) Nat.cast_one (Eq.refl 2))))) half_lt_self_iff._simp_1) (eq_true (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl false))))hpos: (n : ), 0 < n 2 2 ^ n := fun n hn => Eq.mp (congrArg (fun x => x 2 ^ n) (Eq.trans (congrArg (HPow.hPow 2) (zero_add 1)) (pow_one 2))) (pow_le_pow_right₀ (Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl true)) hn)key:∑' (n : ℕ+), 1 / (2 ^ n - 1) = ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ nhsummL:Summable fun n => 1 / (2 ^ n - 1) := Summable.of_nonneg_of_le (fun n => have this := one_le_pow₀ one_le_two; div_nonneg (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le this) (Mathlib.Tactic.Linarith.sub_neg_of_lt a))))) (fun n => Or.casesOn (Nat.eq_zero_or_pos n) (fun h => of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrArg (HDiv.hDiv 1) (Eq.trans (congrArg (fun x => x - 1) (Eq.trans (congrArg (HPow.hPow 2) h) (pow_zero 2))) (sub_self 1))) (div_zero 1))) (Eq.trans (congrArg (HMul.hMul 2) (Eq.trans (congr (congrArg HPow.hPow (one_div 2)) h) (pow_zero 2⁻¹))) (mul_one 2))) (Nat.ofNat_nonneg._simp_1 2))) fun h => have h2 := hpos n h; Eq.mpr (id (congrArg (fun _a => 1 / (2 ^ n - 1) _a) (have this := Eq.mpr (id (congrArg (fun _a => 2 * _a = 2 / 2 ^ n) (div_pow 1 2 n))) (Eq.mpr (id (congrArg (fun _a => 2 * (_a / 2 ^ n) = 2 / 2 ^ n) (one_pow n))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.div_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.div_pf (Mathlib.Tactic.Ring.inv_single (Mathlib.Tactic.Ring.inv_mul (Eq.refl (Nat.rawCast 2 + 0)⁻¹) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNat.of_raw 1))))) (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0)⁻¹ (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0)⁻¹ ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))))); this))) (Eq.mpr (id (congrArg (fun _a => _a) (propext (div_le_div_iff₀ (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Eq.refl (Int.ofNat 1))))) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a)))) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n))))) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 2))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0)))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 2 + 0))))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf n) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (n ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (n ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 2)) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (n ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Mathlib.Tactic.Linarith.sub_nonpos_of_le h2) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))))) (Summable.mul_left 2 (summable_geometric_of_norm_lt_one hr))hsummR:Summable fun n => n.divisors.card / 2 ^ n := Summable.of_nonneg_of_le (fun n => Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos (Nat.cast_nonneg' n.divisors.card) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)) (fun n => Eq.mpr (id (congrArg (fun _a => n.divisors.card / 2 ^ n _a * (1 / 2) ^ n) (pow_one n))) (Eq.mpr (id (congrArg (fun _a => n.divisors.card / 2 ^ n n * _a) (have this := Eq.mpr (id (congrArg (fun _a => _a = 1 / 2 ^ n) (div_pow 1 2 n))) (Eq.mpr (id (congrArg (fun _a => _a / 2 ^ n = 1 / 2 ^ n) (one_pow n))) (Eq.refl (1 / 2 ^ n))); this))) (Eq.mpr (id (congrArg (fun _a => n.divisors.card / 2 ^ n _a) (mul_one_div (↑n) (2 ^ n)))) (div_le_div_of_nonneg_right (Nat.mono_cast (cast (Eq.refl (n.divisors.card n)) (Nat.card_divisors_le_self n))) (le_of_lt (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)))))) (summable_pow_mul_geometric_of_norm_lt_one 1 hr)1 / (2 ^ 0 - 1) + ∑' (n : ℕ+), 1 / (2 ^ n - 1) = (Nat.divisors 0).card / 2 ^ 0 + ∑' (n : ℕ+), (↑n).divisors.card / 2 ^ n All goals completed! 🐙

Show that $$ \sum_{n} \frac{d(n)}{2^n} $$ is irrational.

[Er48] Erdős, P., On arithmetical properties of Lambert series. J. Indian Math. Soc. (N.S.) (1948), 63-66.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_257.variants.tsum_top : Irrational <| ∑' n, n.divisors.card / (2 ^ n : ) := Irrational (∑' (n : ), n.divisors.card / 2 ^ n) All goals completed! 🐙 end Erdos257