awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
rw : (↑(↑(Fin.last b) : ℕ) : ℝ) * ((HSub.hSub (α := ℝ) 1 (↑(b + 1) : ℝ)⁻¹)⁻¹ - 1) = 1
⊢ HMul.hMul (α := ℝ) (↑(↑(Fin.last b) : ℕ) : ℝ) (∑' (i : ℕ), HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (i + 1)) = 1

Tactic:
rw [geom_series_succ _ (by simp [inv_lt_one_iff₀, this]),
      tsum_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, NeZero.pos b])]

Premises used: geom_series_succ, tsum_geometric_of_lt_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
push_cast : (↑b : ℝ) * ((1 - (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1)⁻¹)⁻¹ - 1) = 1
⊢ (↑(↑(Fin.last b) : ℕ) : ℝ) * ((HSub.hSub (α := ℝ) 1 (↑(b + 1) : ℝ)⁻¹)⁻¹ - 1) = 1

Tactic:
push_cast
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ Ne (α := ℝ) (↑b : ℝ) 0

Tactic:
have : (b : ℝ) ≠ 0 := mod_cast NeZero.ne b
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this_1 : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
this : Ne (α := ℝ) (↑b : ℝ) 0
⊢ (↑b : ℝ) * ((1 - (HAdd.hAdd (α := ℝ) (↑b : ℝ) 1)⁻¹)⁻¹ - 1) = 1

Tactic:
field [*]
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
hf : Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ (n + 1)

Tactic:
rw [summable_nat_add_iff (f := fun n ↦ ((b + 1 : ℕ) : ℝ)⁻¹ ^ n) 1]

Premises used: summable_nat_add_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
inst : NeZero b
this : 1 < |HAdd.hAdd (α := ℝ) (↑b : ℝ) 1|
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑(b + 1) : ℝ)⁻¹ n

Tactic:
apply summable_geometric_of_lt_one (by positivity) (by simp [inv_lt_one_iff₀, NeZero.pos b])

Premises used: summable_geometric_of_lt_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
⊢ (ofDigits (b := b - 1 + 1) fun (x : ℕ) ↦ Fin.last (b - 1)) = 1

Tactic:
ofDigits_const_last_eq_one (b - 1)

Premises used: Real.ofDigits_const_last_eq_one, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
h : b = b - 1 + 1
convert! : NeZero (b - 1)
⊢ (ofDigits (b := b) fun (x : ℕ) ↦ (⟨b - 1, ⋯⟩ : Fin b)) = 1

Tactic:
convert! ofDigits_const_last_eq_one (b - 1)
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
⊢ b = b - 1 + 1

Tactic:
grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
out : b - 1 ≠ 0
⊢ NeZero (b - 1)

Tactic:
constructor
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
⊢ b - 1 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
⊢ b ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
⊢ NeZero b

Tactic:
have : NeZero b := ⟨by grind⟩
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
pos : ∀ (hy' : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) y), y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
neg : ∀ (hy' : y ∉ Set.Ico 0 1), y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ
⊢ y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ

Tactic:
by_cases hy' : y ∈ Set.Ico 0 1

Premises used: Set.Ico, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) y
h : Membership.mem (γ := Set (ℕ → Fin b)) Set.univ (y.digits b) ∧ ofDigits (y.digits b) = y
⊢ y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ

Tactic:
use digits y b

Premises used: Real.digits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : Membership.mem (γ := Set ℝ) (Set.Ico 0 1) y
⊢ Membership.mem (γ := Set (ℕ → Fin b)) Set.univ (y.digits b) ∧ ofDigits (y.digits b) = y

Tactic:
simp [ofDigits_digits hb hy']

Premises used: Real.ofDigits_digits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : y ∉ Set.Ico 0 1
⊢ y = 1

Tactic:
grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : y ∉ Set.Ico 0 1
neg : ∃ (y : ℕ → Fin b), ofDigits y = 1
⊢ y ∈ Set.image (α := ℕ → Fin b) ofDigits Set.univ

Tactic:
simp only [Set.image_univ, show y = 1 by grind, Set.mem_range]

Premises used: Set.image_univ, Set.mem_range
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : y ∉ Set.Ico 0 1
⊢ ∃ (y : ℕ → Fin b), ofDigits y = 1

Tactic:
⟨_, ofDigits_const_last_eq_one' hb⟩

Premises used: Exists.intro, Real.ofDigits_const_last_eq_one'
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
hb : 1 < b
this : NeZero b
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) y
hy' : y ∉ Set.Ico 0 1
⊢ ∃ (y : ℕ → Fin b), ofDigits y = 1

Tactic:
exact ⟨_, ofDigits_const_last_eq_one' hb⟩
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
⊢ Continuous (X := ℕ → Fin 0) ofDigits

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
⊢ Continuous (X := ℕ → Fin 1) ofDigits

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b n : ℕ
⊢ 0 < n + 2 ∧ 1 < n + 2

Tactic:
grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b n : ℕ
⊢ 0 < n + 2

Tactic:
obtain ⟨hb0, hb⟩ : 0 < n + 2 ∧ 1 < n + 2 := by grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b n : ℕ
hb0 : 0 < n + 2
⊢ 1 < n + 2

Tactic:
obtain ⟨hb0, hb⟩ : 0 < n + 2 ∧ 1 < n + 2 := by grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b n : ℕ
hb0 : 0 < n + 2
hb : 1 < n + 2
generalize : ∀ (b : ℕ) (hb : 1 < b), Continuous (X := ℕ → Fin b) ofDigits
⊢ Continuous (X := ℕ → Fin (n + 2)) ofDigits

Tactic:
generalize n + 2 = b at hb
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n : ℕ
hb0 : 0 < n + 2
b : ℕ
hb : 1 < b
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
rify at hb0 hb
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n : ℕ
hb0 : 0 < n + 2
b : ℕ
hb : 1 < b
hb0₁ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ LT.lt (α := ℝ) 1 (↑b : ℝ)

Tactic:
rify at hb0 hb
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Continuous (X := ℕ → Fin b) ofDigits

Tactic:
continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_

Premises used: continuous_tsum, Real.ofDigits
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
refine_1 : ∀ (i : ℕ), Continuous (Y := ℝ) fun (x : ℕ → Fin b) ↦ ofDigitsTerm x i
refine_2 : Summable (α := ℝ) fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i
refine_3 : ∀ (n : ℕ) (x : ℕ → Fin b), ‖ofDigitsTerm x n‖ ≤ (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) n
⊢ Continuous (X := ℕ → Fin b) ofDigits

Tactic:
refine continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_

Premises used: continuous_tsum
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ ∀ (i : ℕ), Continuous (Y := ℝ) fun (x : ℕ → Fin b) ↦ (↑(↑(x i) : ℕ) : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (i + 1))⁻¹

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ LE.le (α := ℝ) 0 (↑b : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i

Tactic:
exact summable_geometric_of_lt_one (by positivity) (inv_lt_one_of_one_lt₀ hb)

Premises used: inv_lt_one_of_one_lt₀, summable_geometric_of_lt_one
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
refine_3 : ofDigitsTerm x n ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
⊢ ‖ofDigitsTerm x n‖ ≤ (fun (i : ℕ) ↦ HPow.hPow (α := ℝ) (↑b : ℝ)⁻¹ i) n

Tactic:
simp only [norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg, inv_pow]

Premises used: inv_pow, Real.ofDigitsTerm_nonneg, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
refine_3 : HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
⊢ ofDigitsTerm x n ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹

Tactic:
apply ofDigitsTerm_le.trans

Premises used: Real.ofDigitsTerm_le, LE.le.trans
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
hbc : HSub.hSub (α := ℝ) (↑b : ℝ) 1 ≤ (↑b : ℝ)
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤
    (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹

Tactic:
gcongr
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
linarith : (↑b : ℝ) < HSub.hSub (α := ℝ) (↑b : ℝ) 1 → -1 + ((↑b : ℝ) - HSub.hSub (α := ℝ) (↑b : ℝ) 1) = 0
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 ≤ (↑b : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
⊢ (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ = (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹

Tactic:
grind
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b_1 n_1 b : ℕ
hb0 : 0 < HAdd.hAdd (α := ℝ) (↑n_1 : ℝ) 2
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
n : ℕ
x : ℕ → Fin b
_ :
  HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤
    (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹
_₁ : (↑b : ℝ) * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ = (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹
⊢ HSub.hSub (α := ℝ) (↑b : ℝ) 1 * (HPow.hPow (α := ℝ) (↑b : ℝ) (n + 1))⁻¹ ≤ (HPow.hPow (α := ℝ) (↑b : ℝ) n)⁻¹

Tactic:
calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind

Premises used: Nat.cast, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.OfDigits
Goal:
b : ℕ
⊢ Continuous (X := ℕ → Fin b) ofDigits

Tactic:
match b with
  | 0 => fun_prop
  | 1 => fun_prop
  | n + 2 =>
    obtain ⟨hb0, hb⟩ : 0 < n + 2 ∧ 1 < n + 2 := by grind
    generalize n + 2 = b at hb
    rify at hb0 hb
    refine continuous_tsum (u := fun i ↦ (b : ℝ)⁻¹ ^ i) ?_ ?_ fun n x ↦ ?_
    · simp only [ofDigitsTerm]
      fun_prop
    · exact summable_geometric_of_lt_one (by positivity) (inv_lt_one_of_one_lt₀ hb)
    · simp only [norm_eq_abs, abs_of_nonneg ofDigitsTerm_nonneg, inv_pow]
      apply ofDigitsTerm_le.trans
      calc
        _ ≤ b * ((b : ℝ) ^ (n + 1))⁻¹ := by
          gcongr
          linarith
        _ = _ := by
          grind
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
rw : sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) < π / HPow.hPow (α := ℝ) 2 (n + 2)
rw₁ : 0 < HPow.hPow (α := ℝ) 2 (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π

Tactic:
rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]

Premises used: lt_div_iff₀, Real.sin_pi_over_two_pow_succ
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
h : 0 < π / HPow.hPow (α := ℝ) 2 (n + 2)
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) < π / HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
apply sin_lt

Premises used: Real.sin_lt
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
h : 0 < HPow.hPow (α := ℝ) 2 (n + 2)
⊢ 0 < π / HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
apply div_pos pi_pos

Premises used: Real.pi_pos, div_pos
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
h : 0 < HPow.hPow (α := ℝ) 2 (n + 2)
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) < π / HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
focus
      apply sin_lt
      apply div_pos pi_pos

Premises used: Real.sin_lt, Real.pi_pos, div_pos
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
h : LT.lt (α := ℝ) 0 2
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
apply pow_pos

Premises used: pow_pos
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ LT.lt (α := ℝ) 0 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
ha : LT.lt (α := ℝ) 0 2
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
apply pow_pos

Premises used: pow_pos
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π

Tactic:
have : √(2 - sqrtTwoAddSeries 0 n) / 2 * 2 ^ (n + 2) < π := by
    rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
    focus
      apply sin_lt
      apply div_pos pi_pos
    all_goals apply pow_pos; norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Tactic:
lt_of_le_of_lt (le_of_eq ?_) this

Premises used: lt_of_le_of_lt, le_of_eq
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
refine :
  HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) =
    √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π

Tactic:
refine lt_of_le_of_lt (le_of_eq ?_) this

Premises used: lt_of_le_of_lt, le_of_eq
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
h : Ne (α := ℝ) 2 0
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) =
    √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
rw [pow_succ' _ (n + 1), ← mul_assoc, div_mul_cancel₀, mul_comm]

Premises used: div_mul_cancel₀, mul_assoc, HAdd.hAdd, mul_comm, OfNat.ofNat, pow_succ'
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
⊢ Ne (α := ℝ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
rw :
  π / HPow.hPow (α := ℝ) 2 (n + 2) - sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) <
    1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4
⊢ π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
rw [← div_lt_iff₀ (by simp), ← sin_pi_over_two_pow_succ, ← sub_lt_iff_lt_add']

Premises used: div_lt_iff₀, sub_lt_iff_lt_add', Real.sin_pi_over_two_pow_succ
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ 0 < π / HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ 0 ≤ HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
hab : π ≤ 4
⊢ HPow.hPow (β := ℕ) (π / HPow.hPow (α := ℝ) 2 (n + 2)) 3 / 4 ≤
    HPow.hPow (β := ℕ) (4 / HPow.hPow (α := ℝ) 2 (n + 2)) 3 / 4

Tactic:
gcongr
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ π ≤ 4

Tactic:
pi_le_four

Premises used: Real.pi_le_four
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ π ≤ 4

Tactic:
exact pi_le_four

Premises used: Real.pi_le_four
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
simp :
  HPow.hPow (β := ℕ) (4 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 / HPow.hPow (α := ℝ) 2 n) 3 =
    (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3)⁻¹
⊢ HPow.hPow (β := ℕ) (4 / HPow.hPow (α := ℝ) 2 (n + 2)) 3 / 4 = 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4

Tactic:
simp [add_comm n, pow_add, div_mul_eq_div_div]

Premises used: pow_add, add_comm, div_mul_eq_div_div
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) (4 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 / HPow.hPow (α := ℝ) 2 n) 3 =
    (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3)⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
π : π ≤ HPow.hPow (α := ℝ) 2 (n + 2)
⊢ π / HPow.hPow (α := ℝ) 2 (n + 2) - sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) <
    1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4

Tactic:
calc
      π / 2 ^ (n + 2) - sin (π / 2 ^ (n + 2)) < (π / 2 ^ (n + 2)) ^ 3 / 4 :=
        sub_lt_comm.1 <| sin_gt_sub_cube (by positivity) <| div_le_one_of_le₀ ?_ (by positivity)
      _ ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4 := by gcongr; exact pi_le_four
      _ = 1 / (2 ^ n) ^ 3 / 4 := by simp [add_comm n, pow_add, div_mul_eq_div_div]; norm_num

Premises used: div_le_one_of_le₀, Real.pi, sub_lt_comm, Real.sin_gt_sub_cube, HDiv.hDiv, HPow.hPow, HAdd.hAdd, Iff.mp, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ 4 = HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2)

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
ha : LE.le (α := ℝ) 1 2
hmn : 0 ≤ n
⊢ HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2) ≤ HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ LE.le (α := ℝ) 1 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ 0 ≤ n

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
π : 4 = HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2)
π₁ : HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2) ≤ HPow.hPow (α := ℝ) 2 (n + 2)
⊢ π ≤ HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
calc
      π ≤ 4 := pi_le_four
      _ = 2 ^ (0 + 2) := by norm_num
      _ ≤ 2 ^ (n + 2) := by gcongr <;> norm_num

Premises used: Real.pi_le_four, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
⊢ π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
have : π < (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / (2 ^ n) ^ 3 / 4) * (2 : ℝ) ^ (n + 2) := by
    rw [← div_lt_iff₀ (by simp), ← sin_pi_over_two_pow_succ, ← sub_lt_iff_lt_add']
    calc
      π / 2 ^ (n + 2) - sin (π / 2 ^ (n + 2)) < (π / 2 ^ (n + 2)) ^ 3 / 4 :=
        sub_lt_comm.1 <| sin_gt_sub_cube (by positivity) <| div_le_one_of_le₀ ?_ (by positivity)
      _ ≤ (4 / 2 ^ (n + 2)) ^ 3 / 4 := by gcongr; exact pi_le_four
      _ = 1 / (2 ^ n) ^ 3 / 4 := by simp [add_comm n, pow_add, div_mul_eq_div_div]; norm_num
    calc
      π ≤ 4 := pi_le_four
      _ = 2 ^ (0 + 2) := by norm_num
      _ ≤ 2 ^ (n + 2) := by gcongr <;> norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
⊢ π < HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n

Tactic:
lt_of_lt_of_le this (le_of_eq ?_)

Premises used: le_of_eq, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
refine :
  (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2) =
    HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n
⊢ π < HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n

Tactic:
refine lt_of_lt_of_le this (le_of_eq ?_)

Premises used: le_of_eq, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
rw :
  √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) +
      1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4 * HPow.hPow (α := ℝ) 2 (n + 2) =
    HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n
⊢ (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2) =
    HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
e_a :
  √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) =
    HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n)
e_a₁ : 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4 * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 4 n
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) +
      1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4 * HPow.hPow (α := ℝ) 2 (n + 2) =
    HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n

Tactic:
congr 1
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) =
    HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
⊢ 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
e_a : 1 / HPow.hPow (α := ℝ) 2 (n * 3 + 2) * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 2 (2 * n)
⊢ 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4 * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 4 n

Tactic:
simp only [show (4 : ℝ) = 2 ^ 2 by norm_num, ← pow_mul, div_div, ← pow_add]

Premises used: pow_add, pow_mul, div_div
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
e_a : HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)
e_a₁ : HPow.hPow (α := ℝ) 2 (2 * n) ≠ 0
e_a₂ : HPow.hPow (α := ℝ) 2 (n * 3 + 2) ≠ 0
⊢ 1 / HPow.hPow (α := ℝ) 2 (n * 3 + 2) * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 2 (2 * n)

Tactic:
rw [one_div, one_div, inv_mul_eq_iff_eq_mul₀, eq_comm, mul_inv_eq_iff_eq_mul₀, ← pow_add]

Premises used: inv_mul_eq_iff_eq_mul₀, pow_add, eq_comm, one_div, mul_inv_eq_iff_eq_mul₀
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
e_a : HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + (2 + 2 * n))
e_a₁ : HPow.hPow (α := ℝ) 2 (n * 2 + n + 2) = HPow.hPow (α := ℝ) 2 (n + (2 + 2 * n))
e_a₂ : HPow.hPow (α := ℝ) 2 (2 + (n * 2 + n)) = HPow.hPow (α := ℝ) 2 (n + (2 + 2 * n))
e_a₃ : HPow.hPow (α := ℝ) 2 (2 + (n * 2 + n)) = HPow.hPow (α := ℝ) 2 (2 + 2 * n + n)
e_a₄ : HPow.hPow (α := ℝ) 2 (2 + (n * 2 + n)) = HPow.hPow (α := ℝ) 2 (2 + (2 * n + n))
e_a₅ e_a₆ : HPow.hPow (α := ℝ) 2 (2 + (2 * n + n)) = HPow.hPow (α := ℝ) 2 (2 + (2 * n + n))
⊢ HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)

Tactic:
rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n]

Premises used: Nat.mul_succ, add_assoc, add_comm, mul_comm
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (α := ℝ) 2 (2 * n) ≠ 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Bounds
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (α := ℝ) 2 (n * 3 + 2) ≠ 0

Tactic:
norm_num