awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
refine_1 : -1 ≤ x ∧ x ≤ 1
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) x 2

Tactic:
rw [sub_nonneg, sq_le_one_iff_abs_le_one, abs_le]

Premises used: abs_le, sq_le_one_iff_abs_le_one, sub_nonneg
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
⊢ -1 ≤ x ∧ x ≤ 1

Tactic:
⟨hx.1.le, hx.2⟩

Premises used: LT.lt.le, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
⊢ -1 ≤ x ∧ x ≤ 1

Tactic:
exact ⟨hx.1.le, hx.2⟩
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
⊢ 0 ≤ cos (x * (π / 2))

Tactic:
cos_nonneg_of_neg_pi_div_two_le_of_le ?_ ?_

Premises used: Real.cos_nonneg_of_neg_pi_div_two_le_of_le
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
refine_2 : -(π / 2) ≤ x * (π / 2)
refine_2₁ : x * (π / 2) ≤ π / 2
⊢ 0 ≤ cos (x * (π / 2))

Tactic:
refine cos_nonneg_of_neg_pi_div_two_le_of_le ?_ ?_

Premises used: Real.cos_nonneg_of_neg_pi_div_two_le_of_le
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : x * (π / 2) < -(π / 2) → 2 / 2 = 1
nlinarith₁ nlinarith₂ : x * (π / 2) < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₃ : x * (π / 2) < -(π / 2) → 2 / 2 = 1
nlinarith₄ : x * (π / 2) < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : x * (π / 2) < -(π / 2) → GT.gt (α := ℝ) 2 0
nlinarith₆ : x * (π / 2) < -(π / 2) → 1 * x * (1 * π) - -(1 * π) + (0 - (-1 - x) * (0 - π)) = 0
⊢ -(π / 2) ≤ x * (π / 2)

Tactic:
nlinarith [hx.1, hx.2, pi_pos]

Premises used: Real.pi_pos, And.right, And.left
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioc (-1) 1) x
nlinarith : π / 2 < x * (π / 2) → 2 / 2 = 1
nlinarith₁ : π / 2 < x * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₂ : π / 2 < x * (π / 2) → 2 / 2 = 1
nlinarith₃ nlinarith₄ : π / 2 < x * (π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₅ : π / 2 < x * (π / 2) → GT.gt (α := ℝ) 2 0
nlinarith₆ : π / 2 < x * (π / 2) → 1 * π - 1 * x * (1 * π) + (0 - (x - 1) * (0 - π)) = 0
⊢ x * (π / 2) ≤ π / 2

Tactic:
nlinarith [hx.1, hx.2, pi_pos]

Premises used: Real.pi_pos, And.right, And.left
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
rw : ‖I n (π / 2)‖ ≤ 2
⊢ I n (π / 2) ≤ 2

Tactic:
rw [← norm_of_nonneg I_pos.le]

Premises used: LT.lt.le, _private.0.I_pos, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
⊢ 1 * |HSub.hSub (α := ℝ) 1 (-1)| ≤ 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
refine :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (uIoc (-1) 1) x → ‖(1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))‖ ≤ 1
⊢ ‖I n (π / 2)‖ ≤ 2

Tactic:
refine (norm_integral_le_of_norm_le_const ?_).trans (show (1 : ℝ) * _ ≤ _ by norm_num)

Premises used: intervalIntegral.norm_integral_le_of_norm_le_const, LE.le.trans
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (uIoc (-1) 1) x
⊢ -1 < x ∧ x ≤ 1

Tactic:
simp only [uIoc_of_le, neg_le_self_iff, zero_le_one, mem_Ioc] at hx

Premises used: neg_le_self_iff, zero_le_one, Set.mem_Ioc, Set.uIoc_of_le
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
rw : |1 - HPow.hPow (β := ℕ) x 2| ^ n * |cos (x * (π / 2))| ≤ 1
⊢ ‖(1 - HPow.hPow (β := ℕ) x 2) ^ n * cos (x * (π / 2))‖ ≤ 1

Tactic:
rw [norm_eq_abs, abs_mul, abs_pow]

Premises used: abs_mul, Real.norm_eq_abs, abs_pow
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
⊢ |1 - HPow.hPow (β := ℕ) x 2| ^ n * |cos (x * (π / 2))| ≤ 1

Tactic:
mul_le_one₀ (pow_le_one₀ (abs_nonneg _) ?_) (abs_nonneg _) (abs_cos_le_one _)

Premises used: Real.abs_cos_le_one, mul_le_one₀, abs_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
refine : |1 - HPow.hPow (β := ℕ) x 2| ≤ 1
⊢ |1 - HPow.hPow (β := ℕ) x 2| ^ n * |cos (x * (π / 2))| ≤ 1

Tactic:
refine mul_le_one₀ (pow_le_one₀ (abs_nonneg _) ?_) (abs_nonneg _) (abs_cos_le_one _)

Premises used: Real.abs_cos_le_one, mul_le_one₀, pow_le_one₀
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
rw : -1 ≤ 1 - HPow.hPow (β := ℕ) x 2 ∧ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1
⊢ |1 - HPow.hPow (β := ℕ) x 2| ≤ 1

Tactic:
rw [abs_le]

Premises used: abs_le
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
left : -1 ≤ 1 - HPow.hPow (β := ℕ) x 2
right : 1 - HPow.hPow (β := ℕ) x 2 ≤ 1
⊢ -1 ≤ 1 - HPow.hPow (β := ℕ) x 2 ∧ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1

Tactic:
constructor
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
nlinarith : 1 - HPow.hPow (β := ℕ) x 2 < -1 → -1 + (1 - HPow.hPow (β := ℕ) x 2 - -1) + (0 - (-1 - x) * (x - 1)) = 0
⊢ -1 ≤ 1 - HPow.hPow (β := ℕ) x 2

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
n : ℕ
x : ℝ
hx : -1 < x ∧ x ≤ 1
nlinarith : 1 < 1 - HPow.hPow (β := ℕ) x 2 → 0 - HPow.hPow (β := ℕ) x 2 + (1 - (1 - HPow.hPow (β := ℕ) x 2)) = 0
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
a : ℝ
rw : Tendsto (fun (n : ℕ) ↦ a ^ (2 * n + 1) / (↑n ! : ℝ)) atTop (nhds (a * 0))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ a ^ (2 * n + 1) / (↑n ! : ℝ)) atTop (nhds 0)

Tactic:
rw [← mul_zero a]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
a : ℝ
⊢ Tendsto (fun (n : ℕ) ↦ a ^ (2 * n + 1) / (↑n ! : ℝ)) atTop (nhds (a * 0))

Tactic:
((FloorSemiring.tendsto_pow_div_factorial_atTop (a ^ 2)).const_mul a).congr (fun x => ?_)

Premises used: FloorSemiring.tendsto_pow_div_factorial_atTop, Filter.Tendsto.const_mul, HPow.hPow, Filter.Tendsto.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
a : ℝ
refine : ∀ (x : ℕ), a * (HPow.hPow (β := ℕ) a 2 ^ x / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ a ^ (2 * n + 1) / (↑n ! : ℝ)) atTop (nhds (a * 0))

Tactic:
refine ((FloorSemiring.tendsto_pow_div_factorial_atTop (a ^ 2)).const_mul a).congr (fun x => ?_)

Premises used: FloorSemiring.tendsto_pow_div_factorial_atTop, Filter.Tendsto.const_mul, HPow.hPow, Filter.Tendsto.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
a : ℝ
x : ℕ
rw : a * (a ^ (2 * x) / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)
rw₁ : a * a ^ (2 * x) / (↑x ! : ℝ) = a ^ (2 * x + 1) / (↑x ! : ℝ)
rw₂ rw₃ : a * a ^ (2 * x) / (↑x ! : ℝ) = a * a ^ (2 * x) / (↑x ! : ℝ)
⊢ a * (HPow.hPow (β := ℕ) a 2 ^ x / (↑x ! : ℝ)) = a ^ (2 * x + 1) / (↑x ! : ℝ)

Tactic:
rw [← pow_mul, mul_div_assoc', _root_.pow_succ']

Premises used: mul_div_assoc', pow_mul, pow_succ'
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
x : ℝ
rw : (∃ (y : ℚ), (↑y : ℝ) = x) → ∃ (a : ℤ) (b : ℕ), 0 < b ∧ x = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ ¬Irrational x → ∃ (a : ℤ) (b : ℕ), 0 < b ∧ x = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
rw [Irrational, not_not, mem_range]

Premises used: Set.mem_range, Classical.not_not, Irrational
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
q : ℚ
⊢ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ)

Tactic:
exact_mod_cast (Rat.num_div_den _).symm

Premises used: Rat.num_div_den, Eq.symm
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
q : ℚ
⊢ ∃ (a : ℤ) (b : ℕ), 0 < b ∧ (↑q : ℝ) = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
exact ⟨q.num, q.den, q.pos, by exact_mod_cast (Rat.num_div_den _).symm⟩
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
apply : Irrational (π / (↑2 : ℝ))
⊢ Irrational π

Tactic:
apply Irrational.of_div_natCast 2

Premises used: Irrational.of_div_natCast, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
by_contra : ∀ (h' : ¬Irrational (π / 2)), False
⊢ Irrational (π / 2)

Tactic:
by_contra h'
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
obtain : ∀ (a : ℤ) (b : ℕ) (hb : 0 < b) (h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)), False
⊢ False

Tactic:
obtain ⟨a, b, hb, h⟩ := not_irrational_exists_rep h'

Premises used: _private.0.not_irrational_exists_rep
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ 0 < HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
have : 0 < (a : ℝ) / b := h ▸ pi_div_two_pos
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
this : 0 < HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑b : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 : ℝ)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : LT.lt (α := ℝ) 0 (↑a : ℝ)), LT.lt (α := ℝ) 0 (↑a : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑a : ℝ)

Tactic:
rwa [lt_div_iff₀ (by positivity), zero_mul] at this

Premises used: lt_div_iff₀, MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ 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
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
n : ℕ
⊢ 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
ha : LT.lt (α := ℝ) 0 (↑a : ℝ)
⊢ ∀ (n : ℕ), 0 < HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)

Tactic:
have k (n : ℕ) : 0 < (a : ℝ) ^ (2 * n + 1) / n ! := by positivity
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 ! : ℝ)
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 ! : ℝ)
⊢ ∀ᶠ (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)
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
h₁ :
  ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) < 1 / 2),
    HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1
⊢ ∀ᶠ (n : ℕ) in atTop, HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1

Tactic:
filter_upwards [this] with n hn
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 ! : ℝ) * 2 < 1

Tactic:
rw [lt_div_iff₀ (zero_lt_two : (0 : ℝ) < 2)] at hn

Premises used: lt_div_iff₀, zero_lt_two
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 ! : ℝ) * 2 < 1
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 ! : ℝ) * 2 < 1
⊢ HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1

Tactic:
exact hn.trans_le' (mul_le_mul_of_nonneg_left (I_le _) (by positivity))

Premises used: LT.lt.trans_le', _private.0.I_le, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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

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))
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) < 1), False
⊢ False

Tactic:
obtain ⟨n, hn⟩ := j.exists

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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
⊢ 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
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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)
⊢ n ≤ 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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)
obtain :
  ∀ (z : ℤ)
    (hz :
      eval₂ (Int.castRingHom ℝ) (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (sinPoly n) *
          HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1) =
        (↑z : ℝ)),
    False
⊢ 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))

Premises used: Int.cast, Real, HMul.hMul, HDiv.hDiv, Polynomial.eval₂, Nat.cast, HAdd.hAdd, Int.castRingHom, LE.le.trans, OfNat.ofNat, _private.0.sinPoly, _private.0.sinPoly_natDegree_le, _private.0.is_integer
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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 : ℝ)
⊢ 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
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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))
⊢ 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

Premises used: Real.sin_pi_div_two, Real.cos_pi_div_two, MulZeroClass.mul_zero, mul_one, add_zero
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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)
⊢ I n (π / 2) * HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ^ (2 * n + 1) =
    (↑n ! : ℝ) * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)

Tactic:
nth_rw 2 [h] at e
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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)
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)
⊢ HPow.hPow (α := ℝ) (↑a : ℝ) (2 * n + 1) / (↑n ! : ℝ) * I n (π / 2) =
    eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * HPow.hPow (α := ℝ) (↑b : ℝ) (2 * n + 1)

Tactic:
simp [field, div_pow] at e ⊢

Premises used: div_pow
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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) * 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:
linear_combination e
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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)

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
-- Module: Mathlib.Analysis.Real.Pi.Irrational
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)
⊢ LT.lt (α := ℝ) 0 (↑z : ℝ) ∧ LT.lt (α := ℝ) (↑z : ℝ) 1

Tactic:
simp [← hz, ← h, ← this, hn', hn]