awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x y : ℂ
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
have s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
Tactic: have s1 := cos_add ((x + y) / 2) ((x - y) / 2)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
have s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
Tactic: have s2 := cos_sub ((x + y) / 2) ((x - y) / 2)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
have s1₁ : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
Tactic: rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1
Cleared hypotheses: s1, s2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x y : ℂ
s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
have s2₁ : cos y = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
Tactic: rw [div_sub_div_same, ← sub_add, add_sub_cancel_left, add_self_div_two] at s2
Cleared hypotheses: s2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos y = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
have rw : cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) -
    (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
  -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
Tactic: rw [s1, s2]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
have calc_1 : cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)
Tactic: calc
    cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
calc_1 : cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
have calc_2 : cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
    (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
Tactic: calc
    cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
calc_1 : cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)
calc_2 :
  cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)
have calc_3 : cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
    (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
  2 * cos ((x + y) / 2) * cos ((x - y) / 2)
Tactic: calc
    cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)
have calc_1 : x = (x + y) / 2 + (x - y) / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
calc_1 : x = (x + y) / 2 + (x - y) / 2
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)
have calc_1₁ : y = (x + y) / 2 - (x - y) / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
have calc_2 : cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
    (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
Tactic: rw [cos_add, cos_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
calc_2 :
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
have calc_2₁ : cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
    (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
    (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
Tactic: rw [cos_add, cos_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₁ : sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₂ : sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
  HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₃ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
  HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₃ :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₄ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₃ :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₄ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₃ :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₄ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I)
rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₆ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₃ :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₄ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I)
rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₆ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₇ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-sinh (x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₃ :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₄ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I)
rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₆ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₇ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-sinh (x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₈ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-(sin x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₃ :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₄ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I)
rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₆ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₇ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-sinh (x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₈ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-(sin x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)
have rw₉ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-(sin x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-(sin x * I)) : ℂ)
Tactic: rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (sin (↑x : ℂ)) = sin (↑x : ℂ)
have rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = sin (↑x : ℂ)
Tactic: rw [← sin_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = sin (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (sin (↑x : ℂ)) = sin (↑x : ℂ)
have rw₁ : sin (↑x : ℂ) = sin (↑x : ℂ)
Tactic: rw [← sin_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (sin (↑x : ℂ)).im = 0
have rw : (↑(sin (↑x : ℂ)).re : ℂ).im = 0
Tactic: rw [← ofReal_sin_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (↑(sin (↑x : ℂ)).re : ℂ).im = 0
⊢ (sin (↑x : ℂ)).im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_sin_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
have rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
Tactic: rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
have rw₁ : cosh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
Tactic: rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₁ :
  cosh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
have rw₂ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
Tactic: rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₁ :
  cosh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₂ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
have rw₃ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I))
Tactic: rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₁ :
  cosh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₂ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₃ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I))
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
have rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
Tactic: rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₁ :
  cosh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₂ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₃ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I))
rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
have rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
Tactic: rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₁ :
  cosh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₂ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₃ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I))
rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
rw₅ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
have rw₆ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
Tactic: rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]