awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
rw :
  HAdd.hAdd (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z)
      (iteratedDerivWithin k (fun (x : ℂ) ↦ -(1 / x)) ℍₒ z) =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
      -(HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)))
hf : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot + -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
      -(HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)))
have hg : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -(1 / x)) ℍₒ z
Tactic: rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -(1 / x)) ℍₒ z
have hg : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -x⁻¹) ℍₒ z
Tactic: simp only [one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -x⁻¹) ℍₒ z
have hg : ContDiffWithinAt ℂ (↑k : WithTop ℕ∞) Inv.inv ℍₒ z
Tactic: apply ContDiffWithinAt.neg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h0 : iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x) ℍₒ z =
  iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: have h0 := iteratedDerivWithin_cot_pi_mul_sub_inv k hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h0₁ : HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
    -HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) =
  iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: rw [iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum hk hz, add_comm] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      -HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have rw : iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
    -HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) =
  iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: rw [← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)), h0]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / (z + (↑n : ℂ)) ^ (k + 1)
have h : ∀ (n : ℤ), 1 / (z + (↑n : ℂ)) ^ (k + 1) = (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: convert! iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow hk hz with n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 1 / (z + (↑n : ℂ)) ^ (k + 1) = (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h : 1 / (z + (↑n : ℂ)) ^ (k + 1) = HPow.hPow (β := ℤ) (z + (↑n : ℂ)) (-(↑(k + 1) : ℤ))
Tactic: rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; lia, zpow_neg_coe_of_pos _ (by lia),
    one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
h : 1 / (z + (↑n : ℂ)) ^ (k + 1) = HPow.hPow (β := ℤ) (z + (↑n : ℂ)) (-(↑(k + 1) : ℤ))
⊢ 1 / (z + (↑n : ℂ)) ^ (k + 1) = (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h₁ : 1 / (z + (↑n : ℂ)) ^ (k + 1) = ((z + (↑n : ℂ)) ^ (k + 1))⁻¹
Tactic: rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; lia, zpow_neg_coe_of_pos _ (by lia),
    one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
h : 1 / (z + (↑n : ℂ)) ^ (k + 1) = HPow.hPow (β := ℤ) (z + (↑n : ℂ)) (-(↑(k + 1) : ℤ))
h₁ : 1 / (z + (↑n : ℂ)) ^ (k + 1) = ((z + (↑n : ℂ)) ^ (k + 1))⁻¹
⊢ 1 / (z + (↑n : ℂ)) ^ (k + 1) = (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h₂ : ((z + (↑n : ℂ)) ^ (k + 1))⁻¹ = ((z + (↑n : ℂ)) ^ (k + 1))⁻¹
Tactic: rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; lia, zpow_neg_coe_of_pos _ (by lia),
    one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ HasStrictDerivAt sin ((cexp (x * I) + cexp (-x * I)) * 2⁻¹) x
have h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹
Tactic: convert!
    ((((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp.sub
              ((hasStrictDerivAt_id x).mul_const I).cexp).mul_const
          I).mul_const
      (2 : ℂ)⁻¹ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹
have h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
Tactic: simp only [id]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₃ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₇ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₇ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₈ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₇ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹
h₈ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₉ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * -1) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₇ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹
h₈ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹
h₉ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * -1) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₁₀ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - -cexp (x * I)) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₇ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹
h₈ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹
h₉ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * -1) * 2⁻¹
h₁₀ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - -cexp (x * I)) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₁₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) + cexp (x * I)) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₇ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹
h₈ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹
h₉ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * -1) * 2⁻¹
h₁₀ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - -cexp (x * I)) * 2⁻¹
h₁₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) + cexp (x * I)) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
have h₁₂ : (cexp (-x * I) + cexp (x * I)) * 2⁻¹ = (cexp (-x * I) + cexp (x * I)) * 2⁻¹
Tactic: rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ HasStrictDerivAt cos (-sin x) x
have simp : HasStrictDerivAt cos (-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹) x
Tactic: simp only [sin, div_eq_mul_inv, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ HasStrictDerivAt cos (-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹) x
have h : -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹
Tactic: convert!
    (((hasStrictDerivAt_id x).mul_const I).cexp.add
          ((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp).mul_const
      (2 : ℂ)⁻¹ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
x : ℂ
⊢ -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹
have h : -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (x * I) * (1 * I) + cexp (-x * I) * (-1 * I)) * 2⁻¹
Tactic: simp only [id]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) sin = iteratedDeriv n cos
⊢ iteratedDeriv (n + 1 + 1) sin = iteratedDeriv (n + 1) cos
have succ : deriv (iteratedDeriv (n + 1) sin) = iteratedDeriv (n + 1) cos
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) sin = iteratedDeriv n cos
succ : deriv (iteratedDeriv (n + 1) sin) = iteratedDeriv (n + 1) cos
⊢ iteratedDeriv (n + 1 + 1) sin = iteratedDeriv (n + 1) cos
have succ₁ : deriv (iteratedDeriv n cos) = iteratedDeriv (n + 1) cos
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
ih : iteratedDeriv (n + 1) sin = iteratedDeriv n cos
succ : deriv (iteratedDeriv (n + 1) sin) = iteratedDeriv (n + 1) cos
succ₁ : deriv (iteratedDeriv n cos) = iteratedDeriv (n + 1) cos
⊢ iteratedDeriv (n + 1 + 1) sin = iteratedDeriv (n + 1) cos
have succ₂ : deriv (iteratedDeriv n cos) = deriv (iteratedDeriv n cos)
Tactic: rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
⊢ iteratedDeriv (n + 1) sin = iteratedDeriv n cos
have zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) sin = iteratedDeriv 0 cos
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv (goal)
Goal:
n : ℕ
zero : iteratedDeriv (HAdd.hAdd (α := ℕ) 0 1) sin = iteratedDeriv 0 cos
⊢ iteratedDeriv (n + 1) sin = iteratedDeriv n cos
have succ : ∀ (n : ℕ) (ih : iteratedDeriv (n + 1) sin = iteratedDeriv n cos),
  iteratedDeriv (n + 1 + 1) sin = iteratedDeriv (n + 1) cos
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iteratedDeriv_succ, ih, iteratedDeriv_succ]
Cleared hypotheses: n