awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
h : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log (↑(1 + g x) : ℂ)
h₁ : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log ((↑1 : ℂ) + (↑(g x) : ℂ))
⊢ (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * (↑(log (1 + g x)) : ℂ)
have h₂ : (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ)) = (↑x : ℂ) * Complex.log (1 + (↑(g x) : ℂ))
Tactic: rw [Complex.ofReal_log (by linarith), Complex.ofReal_add, Complex.ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (hypothesis)
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
⊢ Tendsto (fun (x : ℝ) ↦ (1 + g x) ^ x) atTop (𝓝 (rexp t))
have hg0 : Tendsto g atTop (𝓝 0)
Tactic: have hg0 := tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded
    hg.norm.isBoundedUnder_le (tendsto_id'.mpr (by simp))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ x * g x) atTop (𝓝 t)
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ (1 + g x) ^ x) atTop (𝓝 (rexp t))
have rw : ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))) (hg0 : Tendsto g atTop (𝓝 0)),
  Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (↑(rexp t) : ℂ))
Tactic: rw [← tendsto_ofReal_iff] at hg ⊢
Cleared hypotheses: hg, hg0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg : Tendsto (fun (x : ℝ) ↦ (↑(x * g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
hg0 : Tendsto g atTop (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (↑(rexp t) : ℂ))
have push_cast : ∀ (hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))),
  Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (Complex.exp (↑t : ℂ)))
Tactic: push_cast at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)) atTop (𝓝 (Complex.exp (↑t : ℂ)))
have apply : EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ)) fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)
Tactic: apply (Complex.tendsto_one_add_cpow_exp_of_tendsto hg).congr'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
⊢ EventuallyEq (β := ℂ) atTop (fun (x : ℝ) ↦ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ)) fun (x : ℝ) ↦ (↑((1 + g x) ^ x) : ℂ)
have h : ∀ (x : ℝ) (hg1 : -1 ≤ g x), (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑((1 + g x) ^ x) : ℂ)
Tactic: filter_upwards [hg0.eventually_const_le (show (-1 : ℝ) < 0 by simp)] with x hg1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
⊢ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑((1 + g x) ^ x) : ℂ)
have h : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑(1 + g x) : ℂ) ^ (↑x : ℂ)
Tactic: rw [Complex.ofReal_cpow (by linarith), Complex.ofReal_add, Complex.ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
h : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑(1 + g x) : ℂ) ^ (↑x : ℂ)
⊢ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑((1 + g x) ^ x) : ℂ)
have h₁ : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = ((↑1 : ℂ) + (↑(g x) : ℂ)) ^ (↑x : ℂ)
Tactic: rw [Complex.ofReal_cpow (by linarith), Complex.ofReal_add, Complex.ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
g : ℝ → ℝ
t : ℝ
hg0 : Tendsto g atTop (𝓝 0)
hg : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) * (↑(g x) : ℂ)) atTop (𝓝 (↑t : ℂ))
x : ℝ
hg1 : -1 ≤ g x
h : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑(1 + g x) : ℂ) ^ (↑x : ℂ)
h₁ : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = ((↑1 : ℂ) + (↑(g x) : ℂ)) ^ (↑x : ℂ)
⊢ (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (↑((1 + g x) ^ x) : ℂ)
have h₂ : (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ) = (1 + (↑(g x) : ℂ)) ^ (↑x : ℂ)
Tactic: rw [Complex.ofReal_cpow (by linarith), Complex.ofReal_add, Complex.ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
⊢ Tendsto (fun (x : ℝ) ↦ (1 + t / x) ^ x) atTop (𝓝 (rexp t))
have hg : Tendsto (fun (x : ℝ) ↦ x * (t / x)) atTop (𝓝 t)
Tactic: apply tendsto_one_add_rpow_exp_of_tendsto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
⊢ Tendsto (fun (x : ℝ) ↦ x * (t / x)) atTop (𝓝 t)
have hg : ∀ᶠ (x' : ℝ) in atTop, x' * (t / x') = t
Tactic: apply tendsto_nhds_of_eventually_eq
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogBounds (goal)
Goal:
t : ℝ
⊢ ∀ᶠ (x' : ℝ) in atTop, x' * (t / x') = t
have h : ∀ (x : ℝ) (hx0 : x ≠ 0), x * (t / x) = t
Tactic: filter_upwards [eventually_ne_atTop 0] with x hx0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv (goal)
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun (t : ℂ) ↦ log (f t)) (f' / f x) x
have rw : HasStrictDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x
Tactic: rw [div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv (goal)
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun (t : ℂ) ↦ log (f t)) (f' / f x) x
have rw : HasDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x
Tactic: rw [div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv (goal)
Goal:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun (t : ℂ) ↦ log (f t)) (f' / f x) s x
have rw : HasDerivWithinAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') s x
Tactic: rw [div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv (hypothesis)
Goal:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
⊢ deriv (log ∘ f) x = logDeriv f x
have A : deriv (fun (t : ℂ) ↦ log (f t)) x = deriv f x / f x
Tactic: have A := (HasDerivAt.clog h₁.hasDerivAt h₂).deriv
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (hypothesis)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
⊢ abs (a * b) = abs a * abs b
have hab : Commute (abs a) (abs b)
Tactic: have hab := h₁.cfcAbs_cfcAbs h₂
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
⊢ abs (a * b) = abs a * abs b
have rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
⊢ abs (a * b) = abs a * abs b
have rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
⊢ abs (a * b) = abs a * abs b
have rw₂ : abs b * abs a * (abs b * abs a) = star (a * b) * (a * b)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
rw₂ : abs b * abs a * (abs b * abs a) = star (a * b) * (a * b)
⊢ abs (a * b) = abs a * abs b
have rw₃ : abs b * abs b * (abs a * abs a) = star (a * b) * (a * b)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
rw₂ : abs b * abs a * (abs b * abs a) = star (a * b) * (a * b)
rw₃ : abs b * abs b * (abs a * abs a) = star (a * b) * (a * b)
⊢ abs (a * b) = abs a * abs b
have rw₄ : star b * b * (abs a * abs a) = star (a * b) * (a * b)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
rw₂ : abs b * abs a * (abs b * abs a) = star (a * b) * (a * b)
rw₃ : abs b * abs b * (abs a * abs a) = star (a * b) * (a * b)
rw₄ : star b * b * (abs a * abs a) = star (a * b) * (a * b)
⊢ abs (a * b) = abs a * abs b
have rw₅ : star b * b * (star a * a) = star (a * b) * (a * b)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
rw₂ : abs b * abs a * (abs b * abs a) = star (a * b) * (a * b)
rw₃ : abs b * abs b * (abs a * abs a) = star (a * b) * (a * b)
rw₄ : star b * b * (abs a * abs a) = star (a * b) * (a * b)
rw₅ : star b * b * (star a * a) = star (a * b) * (a * b)
⊢ abs (a * b) = abs a * abs b
have rw₆ : star b * b * (star a * a) = star b * star a * (a * b)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
rw₂ : abs b * abs a * (abs b * abs a) = star (a * b) * (a * b)
rw₃ : abs b * abs b * (abs a * abs a) = star (a * b) * (a * b)
rw₄ : star b * b * (abs a * abs a) = star (a * b) * (a * b)
rw₅ : star b * b * (star a * a) = star (a * b) * (a * b)
rw₆ : star b * b * (star a * a) = star b * star a * (a * b)
⊢ abs (a * b) = abs a * abs b
have rw₇ : star b * star a * (b * a) = star b * star a * (a * b)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a b : A
h₁ : Commute a b
h₂ : Commute a (star b)
hab : Commute (abs a) (abs b)
rw : sqrt (star (a * b) * (a * b)) = abs a * abs b
rw₁ : abs a * abs b * (abs a * abs b) = star (a * b) * (a * b)
rw₂ : abs b * abs a * (abs b * abs a) = star (a * b) * (a * b)
rw₃ : abs b * abs b * (abs a * abs a) = star (a * b) * (a * b)
rw₄ : star b * b * (abs a * abs a) = star (a * b) * (a * b)
rw₅ : star b * b * (star a * a) = star (a * b) * (a * b)
rw₆ : star b * b * (star a * a) = star b * star a * (a * b)
rw₇ : star b * star a * (b * a) = star b * star a * (a * b)
⊢ abs (a * b) = abs a * abs b
have rw₈ : star b * star a * (b * a) = star b * star a * (b * a)
Tactic: rw [abs, CFC.sqrt_eq_iff _ _ (star_mul_self_nonneg _)
    (hab.mul_nonneg (abs_nonneg a) (abs_nonneg b)), hab.eq, hab.mul_mul_mul_comm,
    abs_mul_abs, abs_mul_abs, star_mul, h₂.star_left.symm.mul_mul_mul_comm, h₁.eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : IsStarNormal a
⊢ abs (a * a) = star a * a
have rw : abs a * abs a = star a * a
Tactic: rw [Commute.cfcAbs_mul_eq (.refl a) ha.star_comm_self.symm, abs_mul_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : IsStarNormal a
rw : abs a * abs a = star a * a
⊢ abs (a * a) = star a * a
have rw₁ : star a * a = star a * a
Tactic: rw [Commute.cfcAbs_mul_eq (.refl a) ha.star_comm_self.symm, abs_mul_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
⊢ HPow.hPow (β := ℝ≥0) (abs a) 2 = star a * a
have simp : abs a * abs a = star a * a
Tactic: simp only [abs_nonneg, nnrpow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
x : ℝ≥0
⊢ abs a ^ (2 * x) = (star a * a) ^ x
have rw : HPow.hPow (β := ℝ≥0) (abs a) 2 ^ x = (star a * a) ^ x
Tactic: rw [← nnrpow_nnrpow, abs_nnrpow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
x : ℝ≥0
rw : HPow.hPow (β := ℝ≥0) (abs a) 2 ^ x = (star a * a) ^ x
⊢ abs a ^ (2 * x) = (star a * a) ^ x
have rw₁ : (star a * a) ^ x = (star a * a) ^ x
Tactic: rw [← nnrpow_nnrpow, abs_nnrpow_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
⊢ abs a = a
have rw : sqrt (star a * a) = a
Tactic: rw [abs, ha.star_eq, sqrt_mul_self a ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
rw : sqrt (star a * a) = a
⊢ abs a = a
have rw₁ : sqrt (a * a) = a
Tactic: rw [abs, ha.star_eq, sqrt_mul_self a ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : 0 ≤ a
rw : sqrt (star a * a) = a
rw₁ : sqrt (a * a) = a
⊢ abs a = a
have rw₂ : a = a
Tactic: rw [abs, ha.star_eq, sqrt_mul_self a ha]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : IsSelfAdjoint a
| abs a
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(x * x)) a
Tactic: rw [abs, ha.star_eq, sqrt_eq_real_sqrt .., ← cfcₙ_id' ℝ a, ← cfcₙ_mul .., ← cfcₙ_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ abs a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
have conv_lhs : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(x * x)) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
Tactic: conv_lhs =>
    rw [abs, ha.star_eq, sqrt_eq_real_sqrt .., ← cfcₙ_id' ℝ a, ← cfcₙ_mul .., ← cfcₙ_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs (goal)
Goal:
A : Type u_2
inst : NonUnitalRing A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Module ℝ A
inst_4 : SMulCommClass ℝ A A
inst_5 : IsScalarTower ℝ A A
inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : IsTopologicalRing A
inst_11 : T2Space A
a : A
ha : IsSelfAdjoint a
⊢ a⁺ + a⁻ = abs a
have rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ + x⁻) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
Tactic: rw [CFC.posPart_def, CFC.negPart_def, ← cfcₙ_add .., abs_eq_cfcₙ_norm a ha]