-- 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
θ : ℝ
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) θ

Tactic:
rw [mul_mul_mul_comm, integral_sub, mul_sub, add_sub_assoc]

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 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) +
      ((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 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + (2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ)

case convert_2.convert_2.hf
θ : ℝ
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₂
⊢ IntervalIntegrable (fun x => (2 * ↑n + 1) * (f x ^ n * v₂ x)) volume (-1) 1

case convert_2.convert_2.hg
θ : ℝ
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₂
⊢ IntervalIntegrable (fun x => 2 * ↑n * (f x ^ (n - 1) * v₂ x)) volume (-1) 1

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
⊢ -2 * (↑n + 1) * ∫ (x : ℝ) in -1 ..1, u₂ x * 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:
rw [integral_mul_deriv_eq_deriv_mul (fun x _ => hu₂ x) (fun x _ => hv₂ x)
  (hu₂d.intervalIntegrable _ _) (hv₂d.intervalIntegrable _ _),
  mul_sub, t, neg_mul, neg_mul, neg_mul, sub_neg_eq_add]

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
⊢ -(2 * (↑n + 1) * (2 * (0 ^ n * cos θ))) + 2 * (↑n + 1) * ∫ (x : ℝ) in -1 ..1, u₂' x * v₂ x =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ