awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
have rw : sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) < π / HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
rw : sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) < π / HPow.hPow (α := ℝ) 2 (n + 2)
⊢ √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
have rw₁ : 0 < HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: rw [← lt_div_iff₀, ← sin_pi_over_two_pow_succ]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) < π / HPow.hPow (α := ℝ) 2 (n + 2)
have h : 0 < π / HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: apply sin_lt
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ 0 < π / HPow.hPow (α := ℝ) 2 (n + 2)
have h : 0 < HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: apply div_pos pi_pos
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) < π / HPow.hPow (α := ℝ) 2 (n + 2)
have h : 0 < HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: focus
      apply sin_lt
      apply div_pos pi_pos
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 2)
have h : LT.lt (α := ℝ) 0 2
Tactic: apply pow_pos
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 2)
have ha : LT.lt (α := ℝ) 0 2
Tactic: apply pow_pos
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (hypothesis)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π
have this : √(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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) < π
have refine : HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) =
  √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2)
Tactic: refine lt_of_le_of_lt (le_of_eq ?_) this
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
this : √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) < π
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) =
    √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2)
have h : Ne (α := ℝ) 2 0
Tactic: rw [pow_succ' _ (n + 1), ← mul_assoc, div_mul_cancel₀, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
have rw : π / HPow.hPow (α := ℝ) 2 (n + 2) - sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) <
  1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4
Tactic: rw [← div_lt_iff₀ (by simp), ← sin_pi_over_two_pow_succ, ← sub_lt_iff_lt_add']
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) (π / HPow.hPow (α := ℝ) 2 (n + 2)) 3 / 4 ≤
    HPow.hPow (β := ℕ) (4 / HPow.hPow (α := ℝ) 2 (n + 2)) 3 / 4
have hab : π ≤ 4
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) (4 / HPow.hPow (α := ℝ) 2 (n + 2)) 3 / 4 = 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4
have simp : HPow.hPow (β := ℕ) (4 / HPow.hPow (α := ℝ) (β := ℕ) 2 2 / HPow.hPow (α := ℝ) 2 n) 3 =
  (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3)⁻¹
Tactic: simp [add_comm n, pow_add, div_mul_eq_div_div]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ π / HPow.hPow (α := ℝ) 2 (n + 2) - sin (π / HPow.hPow (α := ℝ) 2 (n + 2)) <
    1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4
have π : π ≤ HPow.hPow (α := ℝ) 2 (n + 2)
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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2) ≤ HPow.hPow (α := ℝ) 2 (n + 2)
have ha : LE.le (α := ℝ) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
ha : LE.le (α := ℝ) 1 2
⊢ HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2) ≤ HPow.hPow (α := ℝ) 2 (n + 2)
have hmn : 0 ≤ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
⊢ π ≤ HPow.hPow (α := ℝ) 2 (n + 2)
have π : 4 = HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2)
Tactic: calc
      π ≤ 4 := pi_le_four
      _ = 2 ^ (0 + 2) := by norm_num
      _ ≤ 2 ^ (n + 2) := by gcongr <;> norm_num
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
π : 4 = HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 2)
⊢ π ≤ HPow.hPow (α := ℝ) 2 (n + 2)
have π₁ : HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 0 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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (hypothesis)
Goal:
n : ℕ
⊢ π < HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n
have this : π <
  (√(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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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
have 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
Tactic: refine lt_of_lt_of_le this (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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 + 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
have 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
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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) +
      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
have e_a : √(2 - sqrtTwoAddSeries 0 n) / 2 * HPow.hPow (α := ℝ) 2 (n + 2) =
  HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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)
⊢ √(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
have e_a₁ : 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4 * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 4 n
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
⊢ 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4 * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 4 n
have e_a : 1 / HPow.hPow (α := ℝ) 2 (n * 3 + 2) * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 2 (2 * n)
Tactic: simp only [show (4 : ℝ) = 2 ^ 2 by norm_num, ← pow_mul, div_div, ← pow_add]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
this :
  π <
    (√(2 - sqrtTwoAddSeries 0 n) / 2 + 1 / HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) 2 n) 3 / 4) *
      HPow.hPow (α := ℝ) 2 (n + 2)
⊢ 1 / HPow.hPow (α := ℝ) 2 (n * 3 + 2) * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 2 (2 * n)
have e_a : HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 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]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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)
⊢ 1 / HPow.hPow (α := ℝ) 2 (n * 3 + 2) * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 2 (2 * n)
have e_a₁ : HPow.hPow (α := ℝ) 2 (2 * n) ≠ 0
Tactic: rw [one_div, one_div, inv_mul_eq_iff_eq_mul₀, eq_comm, mul_inv_eq_iff_eq_mul₀, ← pow_add]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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
⊢ 1 / HPow.hPow (α := ℝ) 2 (n * 3 + 2) * HPow.hPow (α := ℝ) 2 (n + 2) = 1 / HPow.hPow (α := ℝ) 2 (2 * n)
have e_a₂ : HPow.hPow (α := ℝ) 2 (n * 3 + 2) ≠ 0
Tactic: rw [one_div, one_div, inv_mul_eq_iff_eq_mul₀, eq_comm, mul_inv_eq_iff_eq_mul₀, ← pow_add]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)
have e_a : 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]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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))
⊢ HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)
have e_a₁ : HPow.hPow (α := ℝ) 2 (n * 2 + n + 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]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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))
⊢ HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)
have e_a₂ : HPow.hPow (α := ℝ) 2 (2 + (n * 2 + n)) = HPow.hPow (α := ℝ) 2 (n + (2 + 2 * n))
Tactic: rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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))
⊢ HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)
have e_a₃ : HPow.hPow (α := ℝ) 2 (2 + (n * 2 + n)) = HPow.hPow (α := ℝ) 2 (2 + 2 * n + n)
Tactic: rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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)
⊢ HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)
have e_a₄ : HPow.hPow (α := ℝ) 2 (2 + (n * 2 + n)) = HPow.hPow (α := ℝ) 2 (2 + (2 * n + n))
Tactic: rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
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))
⊢ HPow.hPow (α := ℝ) 2 (n * 3 + 2) = HPow.hPow (α := ℝ) 2 (n + 2 + 2 * n)
have e_a₅ : HPow.hPow (α := ℝ) 2 (2 + (2 * n + n)) = HPow.hPow (α := ℝ) 2 (2 + (2 * n + n))
Tactic: rw [add_assoc, Nat.mul_succ, add_comm, add_comm n, add_assoc, mul_comm n]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ a < π
have refine : a ≤ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n)
Tactic: refine lt_of_le_of_lt ?_ (pi_gt_sqrtTwoAddSeries n)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ a ≤ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n)
have rw : a ≤ √(2 - sqrtTwoAddSeries 0 n) * HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ a ≤ √(2 - sqrtTwoAddSeries 0 n) * HPow.hPow (α := ℝ) 2 (n + 1)
have refine : HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ 2 - sqrtTwoAddSeries 0 n
Tactic: refine (div_le_iff₀ (pow_pos (by simp) _)).mp (le_sqrt_of_sq_le ?_)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ 0 = HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)
have rw : 0 = HDiv.hDiv (α := ℝ) 0 (↑1 : ℝ)
Tactic: rw [Nat.cast_zero, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
rw : 0 = HDiv.hDiv (α := ℝ) 0 (↑1 : ℝ)
⊢ 0 = HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [Nat.cast_zero, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n ≤
    2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
⊢ HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ 2 - sqrtTwoAddSeries 0 n
have rwa : sqrtTwoAddSeries 0 n ≤ 2 - HPow.hPow (β := ℕ) (a / HPow.hPow (α := ℝ) 2 (n + 1)) 2
Tactic: rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries (n + 1) ≤ z
have refine : (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries (n + 1) ≤
  (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n
Tactic: refine le_trans ?_ hz
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
⊢ (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)).sqrtTwoAddSeries (n + 1) ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n
have rw : (√(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))).sqrtTwoAddSeries n ≤
  (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n
Tactic: rw [sqrtTwoAddSeries_succ]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
⊢ (√(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))).sqrtTwoAddSeries n ≤
    (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n
have h₁ : √(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ≤ HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
Tactic: apply sqrtTwoAddSeries_monotone_left
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (hypothesis)
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
⊢ √(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ≤ HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
have hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
Tactic: have hb' : 0 < (b : ℝ) := Nat.cast_pos.2 hb
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (hypothesis)
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ √(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ≤ HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
have hd' : LT.lt (α := ℝ) 0 (↑d : ℝ)
Tactic: have hd' : 0 < (d : ℝ) := Nat.cast_pos.2 hd
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
c d a b n : ℕ
z : ℝ
hz : (HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)).sqrtTwoAddSeries n ≤ z
hb : 0 < b
hd : 0 < d
h : (2 * b + a) * HPow.hPow (β := ℕ) d 2 ≤ HPow.hPow (β := ℕ) c 2 * b
hb' : LT.lt (α := ℝ) 0 (↑b : ℝ)
hd' : LT.lt (α := ℝ) 0 (↑d : ℝ)
⊢ √(2 + HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) ≤ HDiv.hDiv (α := ℝ) (↑c : ℝ) (↑d : ℝ)
have h₁ : (HMul.hMul (α := ℝ) 2 (↑b : ℝ) + (↑a : ℝ)) * HPow.hPow (α := ℝ) (β := ℕ) (↑d : ℝ) 2 ≤
  HPow.hPow (α := ℝ) (β := ℕ) (↑c : ℝ) 2 * (↑b : ℝ)
Tactic: rw [sqrt_le_left (div_nonneg c.cast_nonneg d.cast_nonneg), div_pow,
    add_div_eq_mul_add_div _ _ (ne_of_gt hb'), div_le_div_iff₀ hb' (pow_pos hd' _)]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n
h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a
⊢ π < a
have refine : HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n ≤ a
Tactic: refine lt_of_lt_of_le (pi_lt_sqrtTwoAddSeries n) ?_
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n
h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n ≤ a
have rw : 2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
Tactic: rw [← le_sub_iff_add_le, ← le_div_iff₀', sqrt_le_left, sub_le_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n
h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a
rw : 2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n ≤ a
have rw₁ : 0 ≤ (a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: rw [← le_sub_iff_add_le, ← le_div_iff₀', sqrt_le_left, sub_le_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n
h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a
rw : 2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
rw₁ : 0 ≤ (a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)
⊢ HPow.hPow (α := ℝ) 2 (n + 1) * √(2 - sqrtTwoAddSeries 0 n) + 1 / HPow.hPow (α := ℝ) 4 n ≤ a
have rw₂ : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: rw [← le_sub_iff_add_le, ← le_div_iff₀', sqrt_le_left, sub_le_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
n : ℕ
a : ℝ
h :
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries n
h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a
⊢ 2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
have rwa : ∀
  (h :
    2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤
      (HDiv.hDiv (α := ℝ) 0 (↑1 : ℝ)).sqrtTwoAddSeries n)
  (h₂ : 1 / HPow.hPow (α := ℝ) 4 n ≤ a),
  2 - HPow.hPow (β := ℕ) ((a - 1 / HPow.hPow (α := ℝ) 4 n) / HPow.hPow (α := ℝ) 2 (n + 1)) 2 ≤ sqrtTwoAddSeries 0 n
Tactic: rwa [Nat.cast_zero, zero_div] at h
Cleared hypotheses: h, h₂