awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₄ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
  fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
Tactic: simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
h₄ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₅ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
  fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / (↑(2 * n + 1)! : ℂ) / I)
Tactic: simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
h₄ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
h₅ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / (↑(2 * n + 1)! : ℂ) / I)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₆ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
  fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / I / (↑(2 * n + 1)! : ℂ))
Tactic: simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
h₄ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
h₅ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / (↑(2 * n + 1)! : ℂ) / I)
h₆ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / I / (↑(2 * n + 1)! : ℂ))
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₇ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
  fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
Tactic: simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
h₄ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
h₅ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / (↑(2 * n + 1)! : ℂ) / I)
h₆ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / I / (↑(2 * n + 1)! : ℂ))
h₇ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₈ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
  fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
Tactic: simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
h₄ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
h₅ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / (↑(2 * n + 1)! : ℂ) / I)
h₆ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / I / (↑(2 * n + 1)! : ℂ))
h₇ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
h₈ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₉ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
  fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ)
Tactic: simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
z : ℂ
h :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n + 1) * I ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
h₁ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (z ^ (2 * n) * z) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    z ^ (2 * n) * z * (I ^ (2 * n) * I) / (↑(2 * n + 1)! : ℂ) / I
h₂ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (β := ℕ) I 2 ^ n * I) / (↑(2 * n + 1)! : ℂ) / I
h₃ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * (HPow.hPow (α := ℂ) (-1) n * I) / (↑(2 * n + 1)! : ℂ) / I
h₄ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * z / (↑(2 * n + 1)! : ℂ))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * I / (↑(2 * n + 1)! : ℂ) / I
h₅ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / (↑(2 * n + 1)! : ℂ) / I)
h₆ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * (I / I / (↑(2 * n + 1)! : ℂ))
h₇ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (β := ℕ) z 2 ^ n * z * HPow.hPow (α := ℂ) (-1) n * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
h₈ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) * HDiv.hDiv (α := ℂ) 1 (↑(2 * n + 1)! : ℂ)
h₉ :
  Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
    fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * z) / (↑(2 * n + 1)! : ℂ)
⊢ Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * z ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ)) fun (n : ℕ) ↦
    (z * I) ^ (2 * n + 1) / (↑(2 * n + 1)! : ℂ) / I
have h₁₀ : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
  fun (n : ℕ) ↦ HPow.hPow (α := ℂ) (-1) n * (HPow.hPow (β := ℕ) z 2 ^ n * (z / (↑(2 * n + 1)! : ℂ)))
Tactic: simp_rw [mul_pow, pow_succ, pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
    div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
x : ℝ
⊢ cosh x ≤ rexp (HPow.hPow (β := ℕ) x 2 / 2)
have rw : LE.le (α := ℝ) (∑' (n : ℕ), x ^ (2 * n) / (↑(2 * n)! : ℝ))
  ((fun (x : ℝ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℝ)) (HPow.hPow (β := ℕ) x 2 / 2))
Tactic: rw [cosh_eq_tsum, exp_eq_exp_ℝ, exp_eq_tsum ℝ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
x : ℝ
⊢ LE.le (α := ℝ) (∑' (n : ℕ), x ^ (2 * n) / (↑(2 * n)! : ℝ))
    ((fun (x : ℝ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℝ) (↑n ! : ℝ)⁻¹ (x ^ n) : ℝ)) (HPow.hPow (β := ℕ) x 2 / 2))
have refine : ∀ (i : ℕ), x ^ (2 * i) / (↑(2 * i)! : ℝ) ≤ HSMul.hSMul (α := ℝ) (↑i ! : ℝ)⁻¹ ((HPow.hPow (β := ℕ) x 2 / 2) ^ i)
Tactic: refine x.hasSum_cosh.summable.tsum_le_tsum (fun i ↦ ?_) <| expSeries_summable' (x ^ 2 / 2)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
x : ℝ
i : ℕ
⊢ x ^ (2 * i) / (↑(2 * i)! : ℝ) ≤ HSMul.hSMul (α := ℝ) (↑i ! : ℝ)⁻¹ ((HPow.hPow (β := ℕ) x 2 / 2) ^ i)
have simp : HPow.hPow (β := ℕ) x 2 ^ i / (↑(2 * i)! : ℝ) ≤ HPow.hPow (β := ℕ) x 2 ^ i / (HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ))
Tactic: simp only [div_pow, pow_mul, smul_eq_mul, inv_mul_eq_div, div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
x : ℝ
i : ℕ
⊢ HPow.hPow (β := ℕ) x 2 ^ i / (↑(2 * i)! : ℝ) ≤ HPow.hPow (β := ℕ) x 2 ^ i / (HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ))
have hdb : HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ) ≤ (↑(2 * i)! : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Series (goal)
Goal:
x : ℝ
i : ℕ
⊢ HPow.hPow (α := ℝ) 2 i * (↑i ! : ℝ) ≤ (↑(2 * i)! : ℝ)
have hdb : HPow.hPow (α := ℕ) 2 i * i ! ≤ (2 * i)!
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k
have succ : a * a ^ n * u₀ + (a * (b * ∑ k ∈ Finset.range n, a ^ k) + b) = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k
Tactic: rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + (a * (b * ∑ k ∈ Finset.range n, a ^ k) + b) = a * a ^ n * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k
have succ : a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = b * ∑ k ∈ Finset.range (1 + n), a ^ k
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = b * ∑ k ∈ Finset.range (1 + n), a ^ k
have succ : ∑ i ∈ Finset.range n, a * (b * a ^ i) + b = ∑ i ∈ Finset.range n, b * a ^ (i + 1) + b
Tactic: rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ ∑ i ∈ Finset.range n, a * (b * a ^ i) + b = ∑ i ∈ Finset.range n, b * a ^ (i + 1) + b
have succ : ∀ (k : ℕ), a * (b * a ^ k) = b * a ^ (k + 1)
Tactic: congr with k
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
⊢ arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
have zero : arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * u₀ + b * ∑ k ∈ Finset.range 0, a ^ k
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
    congr
    rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]
    congr with k
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : CommSemiring R
n : ℕ
zero : arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * u₀ + b * ∑ k ∈ Finset.range 0, a ^ k
⊢ arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
have succ : ∀ (n : ℕ) (hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k),
  arithGeom a b u₀ (n + 1) = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
    congr
    rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]
    congr with k
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
⊢ arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k
have rw : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ k ∈ Finset.range (n + 1), a ^ k
Tactic: rw [arithGeom_eq_add_sum, Finset.sum_range_succ, mul_add, add_comm, mul_comm _ b]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
rw : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ k ∈ Finset.range (n + 1), a ^ k
⊢ arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k
have rw₁ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * (∑ x ∈ Finset.range n, a ^ x + a ^ n)
Tactic: rw [arithGeom_eq_add_sum, Finset.sum_range_succ, mul_add, add_comm, mul_comm _ b]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
rw : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ k ∈ Finset.range (n + 1), a ^ k
rw₁ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * (∑ x ∈ Finset.range n, a ^ x + a ^ n)
⊢ arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k
have rw₂ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
Tactic: rw [arithGeom_eq_add_sum, Finset.sum_range_succ, mul_add, add_comm, mul_comm _ b]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
rw : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ k ∈ Finset.range (n + 1), a ^ k
rw₁ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * (∑ x ∈ Finset.range n, a ^ x + a ^ n)
rw₂ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
⊢ arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k
have rw₃ : b * ∑ k ∈ Finset.range n, a ^ k + a ^ n * b = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
Tactic: rw [arithGeom_eq_add_sum, Finset.sum_range_succ, mul_add, add_comm, mul_comm _ b]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b : R
inst : CommSemiring R
n : ℕ
rw : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ k ∈ Finset.range (n + 1), a ^ k
rw₁ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * (∑ x ∈ Finset.range n, a ^ x + a ^ n)
rw₂ : a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
rw₃ : b * ∑ k ∈ Finset.range n, a ^ k + a ^ n * b = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
⊢ arithGeom a b b n = b * ∑ k ∈ Finset.range (n + 1), a ^ k
have rw₄ : b * ∑ k ∈ Finset.range n, a ^ k + b * a ^ n = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
Tactic: rw [arithGeom_eq_add_sum, Finset.sum_range_succ, mul_add, add_comm, mul_comm _ b]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)
have succ : a * arithGeom a b u₀ n + b = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)
Tactic: unfold arithGeom
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.ArithmeticGeometric (goal)
Goal:
R : Type u_1
a b u₀ : R
inst : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
have zero : arithGeom a b u₀ 0 = HPow.hPow (β := ℕ) a 0 * (u₀ - b / (1 - a)) + b / (1 - a)
Tactic: induction n with
  | zero => simp
  | succ n hn => unfold arithGeom; grind
Cleared hypotheses: n