awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
⊢ Irrational (π / 2)
have by_contra : ∀ (h' : ¬Irrational (π / 2)), False
Tactic: by_contra h'
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
h' : ¬Irrational (π / 2)
⊢ False
have obtain : ∀ (a : ℤ) (b : ℕ) (hb : 0 < b) (h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)), False
Tactic: obtain ⟨a, b, hb, h⟩ := not_irrational_exists_rep h'
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑a : ℝ)
have this : 0 < HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
Tactic: have : 0 < (a : ℝ) / b := h ▸ pi_div_two_pos
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
this : 0 < HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑a : ℝ)
have rwa : ∀ (this : HMul.hMul (α := ℝ) 0 (↑b : ℝ) < (↑a : ℝ)), LT.lt (α := ℝ) 0 (↑a : ℝ)
Tactic: rwa [lt_div_iff₀ (by positivity), zero_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
this : 0 < HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
rwa : ∀ (this : HMul.hMul (α := ℝ) 0 (↑b : ℝ) < (↑a : ℝ)), LT.lt (α := ℝ) 0 (↑a : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑a : ℝ)
have rwa₁ : ∀ (this : LT.lt (α := ℝ) 0 (↑a : ℝ)), LT.lt (α := ℝ) 0 (↑a : ℝ)
Tactic: rwa [lt_div_iff₀ (by positivity), zero_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ False
have ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
Tactic: have ha : (0 : ℝ) < a := by
    have : 0 < (a : ℝ) / b := h ▸ pi_div_two_pos
    rwa [lt_div_iff₀ (by positivity), zero_mul] at this
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
⊢ False
have k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
Tactic: have k (n : ℕ) : 0 < (a : ℝ) ^ (2 * n + 1) / n ! := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
have this : ∀ᶠ (a_1 : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * a_1 + 1) / (↑a_1 ! : ℝ) < 1 / 2
Tactic: have := (tendsto_pow_div_factorial_at_top_aux a).eventually_lt_const
      (show (0 : ℝ) < 1 / 2 by simp)
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
this : ∀ᶠ (a_1 : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * a_1 + 1) / (↑a_1 ! : ℝ) < 1 / 2
⊢ ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
have h₁ : ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) < 1 / 2),
  HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
Tactic: filter_upwards [this] with n hn
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
this : ∀ᶠ (a_1 : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * a_1 + 1) / (↑a_1 ! : ℝ) < 1 / 2
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) < 1 / 2
⊢ HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
have hn₁ : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * 2 < 1
Tactic: rw [lt_div_iff₀ (zero_lt_two : (0 : ℝ) < 2)] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
⊢ False
have j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
Tactic: have j : ∀ᶠ n : ℕ in atTop, (a : ℝ) ^ (2 * n + 1) / n ! * I n (π / 2) < 1 := by
    have := (tendsto_pow_div_factorial_at_top_aux a).eventually_lt_const
      (show (0 : ℝ) < 1 / 2 by simp)
    filter_upwards [this] with n hn
    rw [lt_div_iff₀ (zero_lt_two : (0 : ℝ) < 2)] at hn
    exact hn.trans_le' (mul_le_mul_of_nonneg_left (I_le _) (by positivity))
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
⊢ False
have obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1), False
Tactic: obtain ⟨n, hn⟩ := j.exists
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
⊢ False
have hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
Tactic: have hn' : 0 < a ^ (2 * n + 1) / n ! * I n (π / 2) := mul_pos (k _) I_pos
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
⊢ False
have obtain : ∀ (z : ℤ)
  (hz :
    eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
        HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
      (↑z : ℝ)),
  False
Tactic: obtain ⟨z, hz⟩ : ∃ z : ℤ, (sinPoly n).eval₂ (Int.castRingHom ℝ) (a / b) * b ^ (2 * n + 1) = z :=
    is_integer a b ((sinPoly_natDegree_le _).trans (by lia))
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
⊢ False
have e : I n (π / 2) * (π / 2) ^ (2 * n + 1) =
  (↑n ! : ℝ) *
    (eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * sin (π / 2) +
      eval₂ (Int.castRingHom ℝ) (π / 2) (cosPoly n) * cos (π / 2))
Tactic: have e := sinPoly_add_cosPoly_eval (π / 2) n
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e :
  I n (π / 2) * (π / 2) ^ (2 * n + 1) =
    (↑n ! : ℝ) *
      (eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * sin (π / 2) +
        eval₂ (Int.castRingHom ℝ) (π / 2) (cosPoly n) * cos (π / 2))
⊢ False
have e₁ : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
Tactic: rw [cos_pi_div_two, sin_pi_div_two, mul_zero, mul_one, add_zero] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
⊢ HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
have e₁ : I n (π / 2) * HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ^ (2 * n + 1) =
  (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
Tactic: nth_rw 2 [h] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e :
  I n (π / 2) * HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ^ (2 * n + 1) =
    (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
⊢ HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
have simp : ∀
  (e :
    I n (π / 2) * HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) =
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) * (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)),
  HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) * I n (π / 2) =
    (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
Tactic: simp [field, div_pow] at e ⊢
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
⊢ False
have this : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
  eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
Tactic: have : a ^ (2 * n + 1) / n ! * I n (π / 2) =
      eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * b ^ (2 * n + 1) := by
    nth_rw 2 [h] at e
    simp [field, div_pow] at e ⊢
    linear_combination e
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this :
  HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
⊢ False
have this₁ : LT.lt (α := ℝ) 0 (↑z : ℝ) ∧ LT.lt (α := ℝ) (↑z : ℝ) 1
Tactic: have : (0 : ℝ) < z ∧ (z : ℝ) < 1 := by simp [← hz, ← h, ← this, hn', hn]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
k : ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)
j : ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
n : ℕ
hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
hn' : 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2)
z : ℤ
hz :
  eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
      HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
    (↑z : ℝ)
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this_1 :
  HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)
this : LT.lt (α := ℝ) 0 (↑z : ℝ) ∧ LT.lt (α := ℝ) (↑z : ℝ) 1
⊢ False
have this₁ : 0 < z ∧ z < 1
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
⊢ ∃ (l : ℝ),
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
have hfa : Antitone (β := ℝ) fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹
Tactic: apply Antitone.tendsto_alternating_series_of_tendsto_zero
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
hfa : Antitone (β := ℝ) fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹
⊢ ∃ (l : ℝ),
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
have hf0 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹) atTop (𝓝 0)
Tactic: apply Antitone.tendsto_alternating_series_of_tendsto_zero
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
x x_1 : ℕ
h : x < x_1
⊢ (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1)⁻¹ ≤ (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1)⁻¹
have hb : 0 < HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
x x_1 : ℕ
h : x < x_1
hb : 0 < HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1
⊢ (HMul.hMul (α := ℝ) 2 (↑x_1 : ℝ) + 1)⁻¹ ≤ (HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1)⁻¹
have hba : LE.le (α := ℝ) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)⁻¹) atTop (𝓝 0)
have hf0 : Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) atTop atTop
Tactic: apply Tendsto.inv_tendsto_atTop
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) atTop atTop
have hf0 : Tendsto (β := ℝ) (fun (x : ℕ) ↦ HMul.hMul (α := ℝ) 2 (↑x : ℝ)) atTop atTop
Tactic: apply tendsto_atTop_add_const_right
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have obtain : ∀ (l : ℝ)
  (h :
    Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)),
  Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
Tactic: obtain ⟨l, h⟩ :
      ∃ l, Tendsto (fun n ↦ ∑ i ∈ range n, (-1 : ℝ) ^ i / (2 * i + 1)) atTop (𝓝 l) := by
    apply Antitone.tendsto_alternating_series_of_tendsto_zero
    · exact antitone_iff_forall_lt.mpr fun _ _ _ ↦ by gcongr
    · apply Tendsto.inv_tendsto_atTop; apply tendsto_atTop_add_const_right
      exact tendsto_natCast_atTop_atTop.const_mul_atTop zero_lt_two
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have abel : Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
  (𝓝 l)
Tactic: have abel := tendsto_tsum_powerSeries_nhdsWithin_lt h
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (hypothesis)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
⊢ Tendsto (fun (k : ℕ) ↦ ∑ i ∈ range k, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop
    (𝓝 (π / 4))
have m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
Tactic: have m : 𝓝[<] (1 : ℝ) ≤ 𝓝 1 := tendsto_nhdsWithin_of_tendsto_nhds fun _ a ↦ a
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
have h1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 1)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
h1 : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝[<] 1)
have h2 : ∀ᶠ (x : ℝ) in 𝓝[<] 1, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 1)
have h1 : Tendsto (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) (𝓝[<] 1) (𝓝 (HPow.hPow (α := ℝ) (β := ℕ) 1 2))
Tactic: nth_rw 3 [← one_pow 2]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] 1, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)
have h2 : ∃ (v : Set ℝ),
  Membership.mem (γ := Filter ℝ) (𝓝[<] 1) v ∧ ∀ y ∈ v, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) y 2)
Tactic: rw [eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
⊢ ∃ (v : Set ℝ),
    Membership.mem (γ := Filter ℝ) (𝓝[<] 1) v ∧
      ∀ y ∈ v, Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) y 2)
have h₁ : Membership.mem (γ := Filter ℝ) (𝓝[<] 1) (Set.Ioo (-1) 1) ∧
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) y 2)
Tactic: use Set.Ioo (-1) 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)
have rwa : HPow.hPow (β := ℕ) x 2 < 1
Tactic: rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
rwa : HPow.hPow (β := ℕ) x 2 < 1
⊢ Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)
have rwa₁ : |x| < 1
Tactic: rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Leibniz (goal)
Goal:
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, HPow.hPow (α := ℝ) (-1) i / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) atTop (𝓝 l)
abel :
  Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), HPow.hPow (α := ℝ) (-1) n / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * x ^ n) (𝓝[<] 1)
    (𝓝 l)
m : LE.le (α := Filter ℝ) (𝓝[<] 1) (𝓝 1)
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
rwa : HPow.hPow (β := ℕ) x 2 < 1
rwa₁ : |x| < 1
⊢ Membership.mem (γ := Set ℝ) (Set.Iio 1) (HPow.hPow (β := ℕ) x 2)
have rwa₂ : -1 < x ∧ x < 1
Tactic: rwa [Set.mem_Iio, sq_lt_one_iff_abs_lt_one, abs_lt, ← Set.mem_Ioo]