-- 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 convert_2.convert_2.e_a
θ : ℝ
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) * ∫ (x : ℝ) in -1 ..1, (2 * ↑n + 1) * (f x ^ n * v₂ x)) -
      2 * (↑n + 1) * ∫ (x : ℝ) in -1 ..1, 2 * ↑n * (f x ^ (n - 1) * v₂ x) =
    2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
simp_rw [integral_const_mul]

Result:
case convert_2.convert_2.e_a
θ : ℝ
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 * ↑n + 1) * ∫ (x : ℝ) in -1 ..1, f x ^ n * v₂ x) -
      2 * (↑n + 1) * (2 * ↑n * ∫ (x : ℝ) in -1 ..1, f x ^ (n - 1) * v₂ x) =
    2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Proof state:
case h.e'_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
⊢ ∫ (x : ℝ) in -1 ..1, -(u₁' x * v₁ x) * θ = ∫ (x : ℝ) in -1 ..1, -2 * (↑n + 1) * (u₂ x * v₂' x)

Tactic:
congr 1 with x

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 : ℝ
⊢ -(u₁' x * v₁ x) * θ = -2 * (↑n + 1) * (u₂ x * v₂' x)

Proof state:
case h.e'_9
θ : ℝ
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
x : ℝ
⊢ u₁' x = ↑(n + 1) * f x ^ (n + 1 - 1) * (-2 * x)

Tactic:
simp only [Nat.add_succ_sub_one, u₁', Nat.cast_add_one]

Result:
case h.e'_9
θ : ℝ
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
x : ℝ
⊢ -(2 * (↑n + 1) * x * f x ^ n) = (↑n + 1) * f x ^ (n + 0) * (-2 * x)

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₂'
⊢ u₁ 1 = 0

Tactic:
simp only [u₁, f]

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₂'
⊢ (1 - 1 ^ 2) ^ (n + 1) = 0