-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
While it is most natural to give the recursive formula for `I (n + 2) θ`, as well as give the second
base case of `I 1 θ`, it is in fact more convenient to give the recursive formula for `I (n + 1) θ`
in terms of `I n θ` and `I (n - 1) θ` (note the natural subtraction!).
Despite the usually inconvenient subtraction, this in fact allows deducing both of the above facts
with significantly fewer analysis computations.
In addition, note the `0 ^ n` on the right hand side - this is intentional, and again allows
combining the proof of the "usual" recursion formula and the base case `I 1 θ`.
-/
private lemma recursion' (n : ℕ) :
    I (n + 1) θ * θ ^ 2 = - (2 * 2 * ((n + 1) * (0 ^ n * cos θ))) +
      2 * (n + 1) * (2 * n + 1) * I n θ - 4 * (n + 1) * n * I (n - 1) θ

Proof state:
case h.e'_2.e_f.h
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
⊢ -(u₁' x * v₁ x) * θ = -2 * (↑n + 1) * (u₂ x * v₂' x)

Tactic:
dsimp [u₁', v₁, u₂, v₂']

Result:
case h.e'_2.e_f.h
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
⊢ -(-(2 * (↑n + 1) * x * f x ^ n) * sin (x * θ)) * θ = -2 * (↑n + 1) * (x * f x ^ n * (-sin (x * θ) * θ))

Proof state:
case convert_2.convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
⊢ -(2 * (↑n + 1) * (2 * (0 ^ n * cos θ))) +
      2 * (↑n + 1) * ∫ (x : ℝ) in -1 ..1, (2 * ↑n + 1) * (f x ^ n * v₂ x) - 2 * ↑n * (f x ^ (n - 1) * v₂ x) =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have : Continuous v₂ := by fun_prop

Result:
case convert_2.convert_2
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this✝ : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
this : Continuous v₂
⊢ -(2 * (↑n + 1) * (2 * (0 ^ n * cos θ))) +
      2 * (↑n + 1) * ∫ (x : ℝ) in -1 ..1, (2 * ↑n + 1) * (f x ^ n * v₂ x) - 2 * ↑n * (f x ^ (n - 1) * v₂ x) =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Proof state:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
let v₂' (x : ℝ) : ℝ := -sin (x * θ) * θ

Result:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Proof state:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have hu₁_eval_neg_one : u₁ (-1) = 0 := by simp only [u₁, f]; simp

Result:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ