-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
For a polynomial `p` with natural degree `≤ k` and integer coefficients, evaluating `p` at a
rational `a / b` gives a rational of the form `z / b ^ k`.
TODO: should this be moved elsewhere? It uses none of the pi-specific definitions.
-/
private lemma is_integer {p : ℤ[X]} (a b : ℤ) {k : ℕ} (hp : p.natDegree ≤ k) :
    ∃ z : ℤ, p.eval₂ (Int.castRingHom ℝ) (a / b) * b ^ k = z

Proof state:
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑z

Tactic:
rcases eq_or_ne b 0 with rfl | hb

Result:
case inl
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑z

Proof state:
case inl.inl
p : ℤ[X]
a : ℤ
hp : p.natDegree ≤ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ 0 = ↑z

Tactic:
exact ⟨p.coeff 0, by simp⟩

Result:
no goals

Proof state:
p : ℤ[X]
a : ℤ
hp : p.natDegree ≤ 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ 0 = ↑(p.coeff 0)

Tactic:
simp

Result:
no goals

Proof state:
case inl
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

Tactic:
rcases k.eq_zero_or_pos with rfl | hk

Result:
case inl.inl
p : ℤ[X]
a : ℤ
hp : p.natDegree ≤ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ 0 = ↑z

case inl.inr
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑z

Tactic:
refine ⟨∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i), ?_⟩

Result:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∑ i ∈ p.support, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) ((monomial i) (p.coeff i)) * ↑b ^ k =
    ∑ x ∈ p.support, ↑(p.coeff x * a ^ x * b ^ (k - x))

Tactic:
simp only [eval₂_monomial, eq_intCast, div_pow, Int.cast_mul, Int.cast_pow]

Result:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∑ x ∈ p.support, ↑(p.coeff x) * (↑a ^ x / ↑b ^ x) * ↑b ^ k = ∑ x ∈ p.support, ↑(p.coeff x) * ↑a ^ x * ↑b ^ (k - x)

Proof state:
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑0

Tactic:
simp [hk.ne']

Result:
no goals

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i

Tactic:
exact dvd_mul_left _ _

Result:
no goals

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (p.sum fun n a => (monomial n) a) * ↑b ^ k =
    ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))

Tactic:
rw [eval₂_sum, sum, Finset.sum_mul, Int.cast_sum]

Result:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∑ i ∈ p.support, eval₂ (Int.castRingHom ℝ) (↑a / ↑b) ((monomial i) (p.coeff i)) * ↑b ^ k =
    ∑ x ∈ p.support, ↑(p.coeff x * a ^ x * b ^ (k - x))

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
⊢ ↑(p.coeff i) * (↑a ^ i / ↑b ^ i) * ↑b ^ k = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)

Tactic:
have ik := (le_natDegree_of_mem_supp i hi).trans hp

Result:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑a ^ i / ↑b ^ i) * ↑b ^ k = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ ↑(p.coeff i) * (↑a ^ i / ↑b ^ i) * ↑b ^ k = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)

Tactic:
rw [mul_assoc, div_mul_comm, ← Int.cast_pow, ← Int.cast_pow, ← Int.cast_pow,
  ← pow_sub_mul_pow b ik, ← Int.cast_div_charZero, Int.mul_ediv_cancel _ (pow_ne_zero _ hb),
  ← mul_assoc, mul_right_comm, ← Int.cast_pow]

Result:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
ik : i ≤ k
⊢ b ^ i ∣ b ^ (k - i) * b ^ i

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ ∑ x ∈ p.support, ↑(p.coeff x) * (↑a ^ x / ↑b ^ x) * ↑b ^ k = ∑ x ∈ p.support, ↑(p.coeff x) * ↑a ^ x * ↑b ^ (k - x)

Tactic:
refine Finset.sum_congr rfl (fun i hi => ?_)

Result:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
i : ℕ
hi : i ∈ p.support
⊢ ↑(p.coeff i) * (↑a ^ i / ↑b ^ i) * ↑b ^ k = ↑(p.coeff i) * ↑a ^ i * ↑b ^ (k - i)

Proof state:
case inl.inr
p : ℤ[X]
a : ℤ
k : ℕ
hp : p.natDegree ≤ k
hk : k > 0
⊢ ∃ z, eval₂ (Int.castRingHom ℝ) (↑a / ↑0) p * ↑0 ^ k = ↑z

Tactic:
exact ⟨0, by simp [hk.ne']⟩

Result:
no goals

Proof state:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑b) p * ↑b ^ k = ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))

Tactic:
conv => lhs; rw [← sum_monomial_eq p]

Result:
case inr
p : ℤ[X]
a b : ℤ
k : ℕ
hp : p.natDegree ≤ k
hb : b ≠ 0
⊢ eval₂ (Int.castRingHom ℝ) (↑a / ↑b) (p.sum fun n a => (monomial n) a) * ↑b ^ k =
    ↑(∑ i ∈ p.support, p.coeff i * a ^ i * b ^ (k - i))