-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
The key lemma: the sequence of integrals `I` can be written as a linear combination of `sin` and
`cos`, with coefficients given by the polynomials `sinPoly` and `cosPoly`.
-/
private lemma sinPoly_add_cosPoly_eval (θ : ℝ) :
    ∀ n : ℕ,
      I n θ * θ ^ (2 * n + 1) = n ! * ((sinPoly n).eval₂ (Int.castRingHom _) θ * sin θ +
        (cosPoly n).eval₂ (Int.castRingHom _) θ * cos θ)
  | 0 => by simp [sinPoly, cosPoly, I_zero]
  | 1 => by simp [I_one, sinPoly, cosPoly, sub_eq_add_neg]
  | n + 2 => by
      calc I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * θ ^ 2 * θ ^ (2 * n + 3)

Proof state:
θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * θ ^ 2 * θ ^ (2 * n + 3)

Tactic:
ring

Result:
no goals

Proof state:
θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ (2 * (n + 2) + 1) =
    ↑(n + 2)! *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)

Tactic:
calc I (n + 2) θ * θ ^ (2 * (n + 2) + 1) = I (n + 2) θ * θ ^ 2 * θ ^ (2 * n + 3) := by ring
  _ = 2 * (n + 2) * (2 * n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (n + 2) * (n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1)) := by rw [recursion]; ring
  _ = _ := by simp [sinPoly_add_cosPoly_eval, sinPoly, cosPoly, Nat.factorial_succ]; ring

Result:
no goals

Proof state:
θ : ℝ
⊢ I 1 θ * θ ^ (2 * 1 + 1) =
    ↑1! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly 1) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly 1) * cos θ)

Tactic:
simp [I_one, sinPoly, cosPoly, sub_eq_add_neg]

Result:
no goals

Proof state:
θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1)) =
    ↑(n + 2)! *
      (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 2)) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 2)) * cos θ)

Tactic:
simp [sinPoly_add_cosPoly_eval, sinPoly, cosPoly, Nat.factorial_succ]

Result:
θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) *
        ((↑n + 1) * ↑n ! *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) * sin θ +
            eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) * cos θ)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 *
        (↑n ! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly n) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly n) * cos θ)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑n !) *
      ((2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (sinPoly n))) *
          sin θ +
        (2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (cosPoly n))) *
          cos θ)

Proof state:
θ : ℝ
n : ℕ
⊢ (2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ) * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))

Tactic:
ring

Result:
no goals

Proof state:
θ : ℝ
⊢ I 0 θ * θ ^ (2 * 0 + 1) =
    ↑0! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly 0) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly 0) * cos θ)

Tactic:
simp [sinPoly, cosPoly, I_zero]

Result:
no goals

Proof state:
θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ 2 * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))

Tactic:
rw [recursion]

Result:
θ : ℝ
n : ℕ
⊢ (2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ) * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))

Proof state:
θ : ℝ
n : ℕ
⊢ 2 * (↑n + 2) * (2 * ↑n + 3) *
        ((↑n + 1) * ↑n ! *
          (eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) * sin θ +
            eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) * cos θ)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 *
        (↑n ! * (eval₂ (Int.castRingHom ℝ) θ (sinPoly n) * sin θ + eval₂ (Int.castRingHom ℝ) θ (cosPoly n) * cos θ)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑n !) *
      ((2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (sinPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (sinPoly n))) *
          sin θ +
        (2 * (2 * ↑n + 3) * eval₂ (Int.castRingHom ℝ) θ (cosPoly (n + 1)) +
            -(4 * θ ^ 2 * eval₂ (Int.castRingHom ℝ) θ (cosPoly n))) *
          cos θ)

Tactic:
ring

Result:
no goals