awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
⊢ Continuous u₂'

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
⊢ Continuous u₂'

Tactic:
have hu₂d : Continuous u₂' := by fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
⊢ Continuous v₂'

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
⊢ Continuous v₂'

Tactic:
have hv₂d : Continuous v₂' := by fun_prop
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
simp : (1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) ^ (n + 1) = 0
⊢ u₁ 1 = 0

Tactic:
simp only [u₁, f]
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
⊢ (1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2) ^ (n + 1) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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:
have hu₁_eval_one : u₁ 1 = 0 := by simp only [u₁, f]; simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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
simp : (1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2) ^ (n + 1) = 0
⊢ u₁ (-1) = 0

Tactic:
simp only [u₁, f]
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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
⊢ (1 - HPow.hPow (α := ℝ) (β := ℕ) (-1) 2) ^ (n + 1) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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
⊢ u₁ (-1) = 0

Tactic:
have hu₁_eval_neg_one : u₁ (-1) = 0 := by simp only [u₁, f]; simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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
⊢ u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)

Tactic:
simp [u₂, v₂, f, ← two_mul]

Premises used: two_mul
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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
⊢ u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (HPow.hPow (α := ℝ) 0 n * cos θ)

Tactic:
have t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ) := by simp [u₂, v₂, f, ← two_mul]
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2) (-((↑2 : ℝ) * x ^ HSub.hSub (α := ℕ) 2 1)) x

Tactic:
(hasDerivAt_pow 2 x).const_sub 1

Premises used: HasDerivAt.const_sub, hasDerivAt_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
x : ℝ
h : -2 * x = -((↑2 : ℝ) * x ^ HSub.hSub (α := ℕ) 2 1)
⊢ HasDerivAt f (-2 * x) x

Tactic:
convert! (hasDerivAt_pow 2 x).const_sub 1 using 1

Premises used: HasDerivAt.const_sub, hasDerivAt_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
x : ℝ
⊢ -2 * x = -((↑2 : ℝ) * x ^ HSub.hSub (α := ℕ) 2 1)

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
⊢ ∀ (x : ℝ), HasDerivAt f (-2 * x) x

Tactic:
have hf (x) : HasDerivAt f (- 2 * x) x := by
    convert! (hasDerivAt_pow 2 x).const_sub 1 using 1
    simp
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
x : ℝ
⊢ HasDerivAt (f ^ (n + 1)) ((↑(n + 1) : ℝ) * f x ^ (n + 1 - 1) * (-2 * x)) x

Tactic:
(hf x).pow _

Premises used: HasDerivAt.pow
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
x : ℝ
h : u₁' x = (↑(n + 1) : ℝ) * f x ^ (n + 1 - 1) * (-2 * x)
⊢ HasDerivAt u₁ (u₁' x) x

Tactic:
convert! (hf x).pow _ using 1

Premises used: HasDerivAt.pow
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
x : ℝ
h : -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * f x ^ (n + 0) * (-2 * 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]

Premises used: Nat.add_succ_sub_one, Nat.cast_add_one
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
x : ℝ
⊢ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * f x ^ (n + 0) * (-2 * x)

Tactic:
ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
⊢ ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x

Tactic:
have hu₁ (x) : HasDerivAt u₁ (u₁' x) x := by
    convert! (hf x).pow _ using 1
    simp only [Nat.add_succ_sub_one, u₁', Nat.cast_add_one]
    ring
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
⊢ ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x

Tactic:
have hv₁ (x) : HasDerivAt v₁ (v₁' x) x := (hasDerivAt_mul_const θ).sin
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
x : ℝ
⊢ HasDerivAt (fun (i : ℝ) ↦ i * f i ^ n) (1 * f x ^ n + x * ((↑n : ℝ) * f x ^ (n - 1) * (-2 * x))) x

Tactic:
(hasDerivAt_id' x).fun_mul ((hf x).fun_pow _)

Premises used: hasDerivAt_id', HasDerivAt.fun_pow, HasDerivAt.fun_mul
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
x : ℝ
h : u₂' x = 1 * f x ^ n + x * ((↑n : ℝ) * f x ^ (n - 1) * (-2 * x))
⊢ HasDerivAt u₂ (u₂' x) x

Tactic:
convert! (hasDerivAt_id' x).fun_mul ((hf x).fun_pow _) using 1

Premises used: hasDerivAt_id', HasDerivAt.fun_pow, HasDerivAt.fun_mul
-- Module: Mathlib.Analysis.Real.Pi.Irrational
Goal:
θ : ℝ
n : ℕ
f : (x : ℝ) → ℝ := fun (x : ℝ) ↦ 1 - HPow.hPow (β := ℕ) x 2
u₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ (n + 1)
u₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n)
v₁ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ sin (x * θ)
v₁' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ) * θ
u₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ x * f x ^ n
u₂' : (x : ℝ) → ℝ := fun (x : ℝ) ↦ f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1)
v₂ : (x : ℝ) → ℝ := fun (x : ℝ) ↦ cos (x * θ)
v₂' : (x : ℝ) → ℝ := 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 * (HPow.hPow (α := ℝ) 0 n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
x : ℝ
h :
  f x ^ n - HMul.hMul (α := ℝ) 2 (↑n : ℝ) * HPow.hPow (β := ℕ) x 2 * f x ^ (n - 1) =
    1 * f x ^ n + x * ((↑n : ℝ) * f x ^ (n - 1) * (-2 * x))
⊢ u₂' x = 1 * f x ^ n + x * ((↑n : ℝ) * f x ^ (n - 1) * (-2 * x))

Tactic:
simp only [u₂']