-- Mathlib/Data/Real/Pi/Irrational.lean
theorem irrational_pi : Irrational π

Proof state:
case intro.intro.intro.intro.intro
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = ↑n ! * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) = eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1)
⊢ False

Tactic:
have : (0 : ℝ) < z ∧ (z : ℝ) < 1 := by simp [← hz, ← h, ← this, hn', hn]

Result:
case intro.intro.intro.intro.intro
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = ↑n ! * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this✝ : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) = eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1)
this : 0 < ↑z ∧ ↑z < 1
⊢ False

Proof state:
case intro.intro.intro.intro.intro
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = ↑n ! * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this✝ : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) = eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1)
this : 0 < ↑z ∧ ↑z < 1
⊢ False

Tactic:
norm_cast at this

Result:
case intro.intro.intro.intro.intro
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
e : I n (π / 2) * (π / 2) ^ (2 * n + 1) = ↑n ! * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
this✝ : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) = eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1)
this : 0 < z ∧ z < 1
⊢ False

Proof state:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
this : ∀ᶠ (a_1 : ℕ) in atTop, ↑a ^ (2 * a_1 + 1) / ↑a_1 ! < 1 / 2
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * 2 < 1
⊢ 0 ≤ ↑a ^ (2 * n + 1) / ↑n !

Tactic:
positivity

Result:
no goals

Proof state:
⊢ Irrational (π / 2)

Tactic:
by_contra h'

Result:
h' : ¬Irrational (π / 2)
⊢ False

Proof state:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
e : I n (π / 2) * (↑a / ↑b) ^ (2 * n + 1) = ↑n ! * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n)
⊢ ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) = eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1)

Tactic:
field_simp at e ⊢

Result:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
ha : 0 < ↑a
k : ∀ (n : ℕ), 0 < ↑a ^ (2 * n + 1) / ↑n !
j : ∀ᶠ (n : ℕ) in atTop, ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
n : ℕ
hn : ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2) < 1
hn' : 0 < ↑a ^ (2 * n + 1) / ↑n ! * I n (π / 2)
z : ℤ
hz : eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (sinPoly n) * ↑b ^ (2 * n + 1) = ↑z
e : I n (π / 2) * ↑a ^ (2 * n + 1) = ↑n ! * eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1)
⊢ ↑a ^ (2 * n + 1) * I n (π / 2) = eval₂ (Int.castRingHom ℝ) (π / 2) (sinPoly n) * ↑b ^ (2 * n + 1) * ↑n !