awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
h :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑0 : ℝ) (↑1 : ℝ)).sqrtTwoAddSeries 11
h₂ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑35839 : ℝ) (↑25342 : ℝ)).sqrtTwoAddSeries 10
h₃ : LT.lt (α := ℕ) 0 25342
h₄ : LT.lt (α := ℕ) 0 1
h₅ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₆ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₇ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑49143 : ℝ) (↑26596 : ℝ)).sqrtTwoAddSeries 9
h₈ : LT.lt (α := ℕ) 0 26596
h₉ : LT.lt (α := ℕ) 0 25342
h₁₀ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₁₁ : LT.lt (α := ℕ) 0 25342
h₁₂ : LT.lt (α := ℕ) 0 1
h₁₃ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₁₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₁₅ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑145729 : ℝ) (↑74292 : ℝ)).sqrtTwoAddSeries 8
h₁₆ : LT.lt (α := ℕ) 0 74292
h₁₇ : LT.lt (α := ℕ) 0 26596
h₁₈ :
  HPow.hPow (α := ℕ) (β := ℕ) 145729 2 * 26596 ≤
    (HMul.hMul (α := ℕ) 2 26596 + 49143) * HPow.hPow (α := ℕ) (β := ℕ) 74292 2
h₁₉ : LT.lt (α := ℕ) 0 26596
h₂₀ : LT.lt (α := ℕ) 0 25342
h₂₁ :
  HPow.hPow (α := ℕ) (β := ℕ) 49143 2 * 25342 ≤
    (HMul.hMul (α := ℕ) 2 25342 + 35839) * HPow.hPow (α := ℕ) (β := ℕ) 26596 2
h₂₂ : LT.lt (α := ℕ) 0 25342
h₂₃ : LT.lt (α := ℕ) 0 1
h₂₄ : HPow.hPow (α := ℕ) (β := ℕ) 35839 2 * 1 ≤ (HMul.hMul (α := ℕ) 2 1 + 0) * HPow.hPow (α := ℕ) (β := ℕ) 25342 2
h₂₅ : 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11 ≤ 3.141593
h₂₆ :
  2 -
      HPow.hPow (β := ℕ)
        ((3.141593 - 1 / HPow.hPow (α := ℝ) (β := ℕ) 4 11) / HPow.hPow (α := ℝ) 2 (HAdd.hAdd (α := ℕ) 11 1)) 2 ≤
    (HDiv.hDiv (α := ℝ) (↑294095 : ℝ) (↑147759 : ℝ)).sqrtTwoAddSeries 7
h₂₇ : LT.lt (α := ℕ) 0 147759
h₂₈ : LT.lt (α := ℕ) 0 74292
⊢ π < 3.141593
have h₂₉ : HPow.hPow (α := ℕ) (β := ℕ) 294095 2 * 74292 ≤
  (HMul.hMul (α := ℕ) 2 74292 + 145729) * HPow.hPow (α := ℕ) (β := ℕ) 147759 2
Tactic: pi_upper_bound [
    35839/25342, 49143/26596, 145729/74292, 294095/147759, 2-137/56868, 2-471/781921, 2-153/1015961,
    2-157/4170049, 2-28/2974805, 2-9/3824747, 2-7/11899211]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
⊢ round π = 3
have refine : π + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1
Tactic: refine round_eq _ |>.trans <| Int.floor_eq_iff.mpr ⟨by grind [pi_gt_three], ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Bounds (goal)
Goal:
⊢ π + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1
have grw : 3.15 + 1 / 2 < HAdd.hAdd (α := ℝ) (↑3 : ℝ) 1
Tactic: grw [pi_lt_d2]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
Goal:
θ : ℝ
⊢ I 0 θ * θ = 2 * sin θ
have rw : θ * ∫ (x : ℝ) in -1..1, HPow.hPow (β := ℕ) (1 - HPow.hPow (β := ℕ) x 2) 0 * cos (x * θ) = 2 * sin θ
Tactic: rw [mul_comm, I]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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 * θ) * θ
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hfd : Continuous f
Tactic: have hfd : Continuous f := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hu₁d : Continuous u₁'
Tactic: have hu₁d : Continuous u₁' := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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₁'
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hv₁d : Continuous v₁'
Tactic: have hv₁d : Continuous v₁' := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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₁'
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hu₂d : Continuous u₂'
Tactic: have hu₂d : Continuous u₂' := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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₂'
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hv₂d : Continuous v₂'
Tactic: have hv₂d : Continuous v₂' := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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₂'
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hu₁_eval_one : u₁ 1 = 0
Tactic: have hu₁_eval_one : u₁ 1 = 0 := by simp only [u₁, f]; simp
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hu₁_eval_neg_one : u₁ (-1) = 0
Tactic: have hu₁_eval_neg_one : u₁ (-1) = 0 := by simp only [u₁, f]; simp
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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
⊢ (∫ (x : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have t : 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]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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
have h : -2 * x = -((↑2 : ℝ) * x ^ HSub.hSub (α := ℕ) 2 1)
Tactic: convert! (hasDerivAt_pow 2 x).const_sub 1 using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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 : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hf : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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
have h : u₁' x = (↑(n + 1) : ℝ) * f x ^ (n + 1 - 1) * (-2 * x)
Tactic: convert! (hf x).pow _ using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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 : ℝ
⊢ u₁' x = (↑(n + 1) : ℝ) * f x ^ (n + 1 - 1) * (-2 * x)
have h : -(2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * x * f x ^ n) = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * f x ^ (n + 0) * (-2 * x)
Tactic: simp only [Nat.add_succ_sub_one, u₁', Nat.cast_add_one]
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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 : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hu₁ : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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 : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
Tactic: have hv₁ (x) : HasDerivAt v₁ (v₁' x) x := (hasDerivAt_mul_const θ).sin
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (goal)
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 u₂ (u₂' x) x
have h : u₂' x = 1 * f x ^ n + x * ((↑n : ℝ) * f x ^ (n - 1) * (-2 * x))
Tactic: convert! (hasDerivAt_id' x).fun_mul ((hf x).fun_pow _) using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Pi.Irrational (hypothesis)
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 : ℝ) in -1..1, (1 - HPow.hPow (β := ℕ) x 2) ^ (n + 1) * cos (x * θ)) * HPow.hPow (β := ℕ) θ 2 =
    -(HMul.hMul (α := ℝ) 2 2 * (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HPow.hPow (α := ℝ) 0 n * cos θ))) +
        2 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) * I n θ -
      4 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n : ℝ) * I (n - 1) θ
have hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
Tactic: have hu₂ (x) : HasDerivAt u₂ (u₂' x) x := by
    convert! (hasDerivAt_id' x).fun_mul ((hf x).fun_pow _) using 1
    simp only [u₂']
    ring