awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Tietze
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)
neg :
  ∀ (g : C(X, E))
    (hg_mem :
      ∀ (x : X), Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((g : (a : X) → E) x : E))
    (hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))), ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f

Tactic:
obtain ⟨g, hg_mem, hg⟩ := (f : C(s, E)).exists_forall_mem_restrict_eq hs hf'

Premises used: toContinuousMap, ContinuousMap.exists_forall_mem_restrict_eq
-- Module: Mathlib.Analysis.Complex.Tietze
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_mem : ∀ (x : X), Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((g : (a : X) → E) x : E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
⊢ ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖

Tactic:
simp only [Metric.mem_closedBall, dist_zero_right] at hg_mem

Premises used: Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.Analysis.Complex.Tietze
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
h :
  ∀ (x : (↑s : Type u)),
    Eq.{w + 1} (α := E) ((g'.restrict s : (a : (↑s : Type u)) → E) x : E) ((f : (a : (↑s : Type u)) → E) x : E)
⊢ g'.restrict s = f

Tactic:
ext x
-- Module: Mathlib.Analysis.Complex.Tietze
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)
⊢ Eq.{w + 1} (α := E) ((g'.restrict s : (a : (↑s : Type u)) → E) x : E) ((f : (a : (↑s : Type u)) → E) x : E)

Tactic:
congrm($(hg) x)
-- Module: Mathlib.Analysis.Complex.Tietze
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
neg : ‖g'‖ = ‖f‖
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f

Tactic:
refine ⟨g', ?_, by ext x; congrm($(hg) x)⟩
-- Module: Mathlib.Analysis.Complex.Tietze
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
⊢ 0 ≤ ‖f‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Tietze
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
neg : ‖f‖ ≤ ‖g'‖
⊢ ‖g'‖ = ‖f‖

Tactic:
apply le_antisymm ((g'.norm_le <| by positivity).mpr hg_mem)

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le, le_antisymm
-- Module: Mathlib.Analysis.Complex.Tietze
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
⊢ 0 ≤ ‖g'‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Tietze
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
neg : ∀ (x : (↑s : Type u)), norm.{w} (E := E) ((f : (a : (↑s : Type u)) → E) x : E) ≤ ‖g'‖
⊢ ‖f‖ ≤ ‖g'‖

Tactic:
refine (f.norm_le <| by positivity).mpr fun x ↦ ?_

Premises used: Iff.mpr, BoundedContinuousFunction.norm_le
-- Module: Mathlib.Analysis.Complex.Tietze
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)
⊢ Eq.{w + 1} (α := E) ((f : (a : (↑s : Type u)) → E) x : E) ((g' : (a : X) → E) (↑x : X) : E)

Tactic:
simpa using congr($(hg) x).symm

Premises used: congrArg, id, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.Tietze
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)
⊢ 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
-- Module: Mathlib.Analysis.Complex.Tietze
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)
neg : norm.{w} (E := E) ((g' : (a : X) → E) (↑x : X) : E) ≤ ‖g'‖
⊢ norm.{w} (E := E) ((f : (a : (↑s : Type u)) → E) x : E) ≤ ‖g'‖

Tactic:
rw [hx]
-- Module: Mathlib.Analysis.Complex.Tietze
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) ((g' : (a : X) → E) (↑x : X) : E) ≤ ‖g'‖

Tactic:
g'.norm_le (norm_nonneg g') |>.mp le_rfl x

Premises used: le_rfl, BoundedContinuousFunction.norm_le, Iff.mp, Subtype.val, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Tietze
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) ((g' : (a : X) → E) (↑x : X) : E) ≤ ‖g'‖

Tactic:
exact g'.norm_le (norm_nonneg g') |>.mp le_rfl x

Premises used: le_rfl, BoundedContinuousFunction.norm_le, Iff.mp, Subtype.val, norm_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ 2 * sinh x = cexp x - cexp (-x)

Tactic:
mul_div_cancel₀ _ two_ne_zero

Premises used: Complex.sinh, mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ 2 * cosh x = cexp x + cexp (-x)

Tactic:
mul_div_cancel₀ _ two_ne_zero

Premises used: mul_div_cancel₀, two_ne_zero, Complex.cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ sinh 0 = 0

Tactic:
simp [sinh]

Premises used: Complex.sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ sinh (-x) = -sinh x

Tactic:
simp [sinh, exp_neg, (neg_div _ _).symm]

Premises used: Complex.sinh, neg_div, Complex.exp_neg, Eq.symm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
a b c d : ℂ
⊢ (a - b) * (c + d) + (a + b) * (c - d) = 2 * (a * c - b * d)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
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))
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh 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]

Premises used: Complex.exp_add, Complex.two_sinh, mul_assoc, neg_add, mul_left_comm, eq_comm, Complex.two_cosh, two_ne_zero', mul_add, mul_right_inj', Complex
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ (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:
sinh_add_aux

Premises used: _private.0.Complex.sinh_add_aux
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ (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:
exact sinh_add_aux

Premises used: _private.0.Complex.sinh_add_aux
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ cosh 0 = 1

Tactic:
simp [cosh]

Premises used: Complex.cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ cosh (-x) = cosh x

Tactic:
simp [add_comm, cosh, exp_neg]

Premises used: Complex.exp_neg, add_comm, Complex.cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
a b c d : ℂ
⊢ (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
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))
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh 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]

Premises used: Complex.exp_add, Complex.two_sinh, mul_assoc, neg_add, mul_left_comm, eq_comm, Complex.two_cosh, two_ne_zero', mul_add, mul_right_inj', Complex
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ (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:
cosh_add_aux

Premises used: _private.0.Complex.cosh_add_aux
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ (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:
exact cosh_add_aux

Premises used: _private.0.Complex.cosh_add_aux
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Tactic:
simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]

Premises used: sub_eq_add_neg, Complex.sinh_neg, Complex.sinh_add, Complex.cosh_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Tactic:
simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]

Premises used: sub_eq_add_neg, Complex.sinh_neg, Complex.cosh_add, Complex.cosh_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
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 : ℂ)
rw₇ rw₈ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x - cexp (-x)) : ℂ) (2 : ℂ)
⊢ sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x)

Tactic:
rw [sinh, ← map_neg, exp_conj, exp_conj, ← map_sub, sinh, map_div₀, map_ofNat]

Premises used: Complex.sinh, map_sub, map_ofNat, map_neg, map_div₀, Complex.exp_conj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = sinh (↑x : ℂ)
rw₁ rw₂ : sinh (↑x : ℂ) = sinh (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (↑x : ℂ)) = sinh (↑x : ℂ)

Tactic:
rw [← sinh_conj, conj_ofReal]

Premises used: Complex.sinh_conj, Complex.conj_ofReal
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(Real.sinh x) : ℂ) = sinh (↑x : ℂ)

Tactic:
ofReal_sinh_ofReal_re _

Premises used: Complex.ofReal_sinh_ofReal_re, Real.sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(sinh (↑x : ℂ)).re : ℂ).im = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (sinh (↑x : ℂ)).im = 0

Tactic:
rw [← ofReal_sinh_ofReal_re, ofReal_im]

Premises used: Complex.ofReal_sinh_ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (sinh (↑x : ℂ)).re = Real.sinh x

Tactic:
rfl

Premises used: Real.sinh, rfl
-- Module: Mathlib.Analysis.Complex.Trigonometric
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 : ℂ)
rw₇ rw₈ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ) =
    HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp x + cexp (-x)) : ℂ) (2 : ℂ)
⊢ cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh x)

Tactic:
rw [cosh, ← map_neg, exp_conj, exp_conj, ← map_add, cosh, map_div₀, map_ofNat]

Premises used: map_ofNat, map_add, map_neg, map_div₀, Complex.exp_conj, Complex.cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cosh (↑x : ℂ)
rw₁ rw₂ : cosh (↑x : ℂ) = cosh (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (↑x : ℂ)) = cosh (↑x : ℂ)

Tactic:
rw [← cosh_conj, conj_ofReal]

Premises used: Complex.cosh_conj, Complex.conj_ofReal
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(Real.cosh x) : ℂ) = cosh (↑x : ℂ)

Tactic:
ofReal_cosh_ofReal_re _

Premises used: Complex.ofReal_cosh_ofReal_re, Real.cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(cosh (↑x : ℂ)).re : ℂ).im = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (cosh (↑x : ℂ)).im = 0

Tactic:
rw [← ofReal_cosh_ofReal_re, ofReal_im]

Premises used: Complex.ofReal_cosh_ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (cosh (↑x : ℂ)).re = Real.cosh x

Tactic:
rfl

Premises used: Real.cosh, rfl
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ tanh x = sinh x / cosh x

Tactic:
rfl

Premises used: Complex.tanh, rfl
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ tanh 0 = 0

Tactic:
simp [tanh]

Premises used: Complex.tanh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ tanh (-x) = -tanh x

Tactic:
simp [tanh, neg_div]

Premises used: Complex.tanh, neg_div
-- Module: Mathlib.Analysis.Complex.Trigonometric
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) : ℂ)
rw₄ rw₅ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x / cosh x) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh x / cosh x) : ℂ)
⊢ tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh x)

Tactic:
rw [tanh, sinh_conj, cosh_conj, ← map_div₀, tanh]

Premises used: Complex.sinh_conj, Complex.tanh, Complex.cosh_conj, map_div₀
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = tanh (↑x : ℂ)
rw₁ rw₂ : tanh (↑x : ℂ) = tanh (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh (↑x : ℂ)) = tanh (↑x : ℂ)

Tactic:
rw [← tanh_conj, conj_ofReal]

Premises used: Complex.tanh_conj, Complex.conj_ofReal