awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ¬‖f‖ = 0
this : TietzeExtension.{u, w} (↑(Metric.closedBall 0 ‖f‖) : Type w)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
g : C(X, E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
hg_mem : ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup (⇑g : (a : X) → E) ⋯ ‖f‖ hg_mem
x : (↑s : Type u)
⊢ norm.{w} (E := E) ((f : (a : (↑s : Type u)) → E) x : E) ≤ ‖g'‖
have hx : Eq.{w + 1} (α := E) ((f : (a : (↑s : Type u)) → E) x : E) ((g' : (a : X) → E) (↑x : X) : E)
Tactic: have hx : f x = g' x := by simpa using congr($(hg) x).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ¬‖f‖ = 0
this : TietzeExtension.{u, w} (↑(Metric.closedBall 0 ‖f‖) : Type w)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
g : C(X, E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
hg_mem : ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup (⇑g : (a : X) → E) ⋯ ‖f‖ hg_mem
x : (↑s : Type u)
hx : Eq.{w + 1} (α := E) ((f : (a : (↑s : Type u)) → E) x : E) ((g' : (a : X) → E) (↑x : X) : E)
⊢ norm.{w} (E := E) ((f : (a : (↑s : Type u)) → E) x : E) ≤ ‖g'‖
have neg : norm.{w} (E := E) ((g' : (a : X) → E) (↑x : X) : E) ≤ ‖g'‖
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y
have rw : (cexp x - cexp (-x)) * (cexp y + cexp (-y)) + (cexp x + cexp (-x)) * (cexp y - cexp (-y)) =
  2 * (cexp x * cexp y - cexp (-x) * cexp (-y))
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), two_sinh, exp_add, neg_add, exp_add, eq_comm, mul_add, ←
    mul_assoc, two_sinh, mul_left_comm, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add,
    mul_left_comm, two_cosh, ← mul_assoc, two_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh y
have rw : (cexp x + cexp (-x)) * (cexp y + cexp (-y)) + (cexp x - cexp (-x)) * (cexp y - cexp (-y)) =
  2 * (cexp x * cexp y + cexp (-x) * cexp (-y))
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, exp_add, neg_add, exp_add, eq_comm, mul_add, ←
    mul_assoc, two_cosh, ← mul_assoc, two_sinh, ← mul_right_inj' (two_ne_zero' ℂ), mul_add,
    mul_left_comm, two_cosh, mul_left_comm, two_sinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw : (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw₁ : (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw₂ : HSub.hSub (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₂ :
  HSub.hSub (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw₃ : HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
    2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₂ :
  HSub.hSub (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₃ :
  HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw₄ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₂ :
  HSub.hSub (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₃ :
  HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₄ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw₅ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) ((cexp x - cexp (-x)) / 2)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₂ :
  HSub.hSub (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₃ :
  HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₄ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₅ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((cexp x - cexp (-x)) / 2)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw₆ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 2 : ℂ)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) - cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₂ :
  HSub.hSub (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₃ :
  HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₄ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
rw₅ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((cexp x - cexp (-x)) / 2)
rw₆ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 2 : ℂ)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)
have rw₇ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ)
Tactic: rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (↑x : ℂ)) = sinh (↑x : ℂ)
have rw : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = sinh (↑x : ℂ)
Tactic: rw [← sinh_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = sinh (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (↑x : ℂ)) = sinh (↑x : ℂ)
have rw₁ : sinh (↑x : ℂ) = sinh (↑x : ℂ)
Tactic: rw [← sinh_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (sinh (↑x : ℂ)).im = 0
have rw : (↑(sinh (↑x : ℂ)).re : ℂ).im = 0
Tactic: rw [← ofReal_sinh_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (↑(sinh (↑x : ℂ)).re : ℂ).im = 0
⊢ (sinh (↑x : ℂ)).im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_sinh_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw : (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw₁ : (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw₂ : HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₂ :
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw₃ : HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
    2 =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₂ :
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₃ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw₄ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₂ :
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₃ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₄ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw₅ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) ((cexp x + cexp (-x)) / 2)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₂ :
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₃ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₄ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₅ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((cexp x + cexp (-x)) / 2)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw₆ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) 2 : ℂ)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp (-(starRingEnd ℂ : (a : ℂ) → ℂ) x)) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₁ :
  (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) x) + cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₂ :
  HAdd.hAdd (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ) (cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (-x))) / 2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₃ :
  HAdd.hAdd (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x) : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (-x)) : ℂ) /
      2 =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₄ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
rw₅ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((cexp x + cexp (-x)) / 2)
rw₆ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) 2 : ℂ)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)
have rw₇ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ)
Tactic: rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (↑x : ℂ)) = cosh (↑x : ℂ)
have rw : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cosh (↑x : ℂ)
Tactic: rw [← cosh_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cosh (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (↑x : ℂ)) = cosh (↑x : ℂ)
have rw₁ : cosh (↑x : ℂ) = cosh (↑x : ℂ)
Tactic: rw [← cosh_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (cosh (↑x : ℂ)).im = 0
have rw : (↑(cosh (↑x : ℂ)).re : ℂ).im = 0
Tactic: rw [← ofReal_cosh_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (↑(cosh (↑x : ℂ)).re : ℂ).im = 0
⊢ (cosh (↑x : ℂ)).im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_cosh_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
have rw : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
Tactic: rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
⊢ tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
have rw₁ : HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x) : ℂ) (cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
Tactic: rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
rw₁ :
  HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x) : ℂ) (cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
⊢ tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
have rw₂ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x) : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
Tactic: rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
rw₁ :
  HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x) : ℂ) (cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
rw₂ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x) : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
⊢ tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
have rw₃ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x / cosh x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x) : ℂ)
Tactic: rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
rw₁ :
  HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x) : ℂ) (cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
rw₂ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x) : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
rw₃ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x / cosh x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x) : ℂ)
⊢ tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)
have rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x / cosh x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x / cosh x) : ℂ)
Tactic: rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh (↑x : ℂ)) = tanh (↑x : ℂ)
have rw : tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = tanh (↑x : ℂ)
Tactic: rw [← tanh_conj, conj_ofReal]