/-
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 FormalConjecturesUtilErdős Problem 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 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 < n⊢ 2 ≤ 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 < n⊢ 1 ≤ 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_two⊢ 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_two⊢ 0 ≤ 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_two⊢ 0 ≤ 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_two⊢ 0 ≤ 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_two⊢ 0 ≤ 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 = 0⊢ 1 / (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 > 0⊢ 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 = 0⊢ 1 / (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 > 0⊢ 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 > 0h2:2 ≤ 2 ^ n := hpos n h⊢ 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 > 0h2:2 ≤ 2 ^ n := hpos n h⊢ 1 * 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.,
@[category research solved, AMS 11]
theorem erdos_257.variants.tsum_top :
Irrational <| ∑' n, n.divisors.card / (2 ^ n : ℝ) := ⊢ Irrational (∑' (n : ℕ), ↑n.divisors.card / 2 ^ n)
All goals completed! 🐙
end Erdos257