awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
⊢ IsOpenMap cexp

Tactic:
isOpenMap_of_hasStrictDerivAt hasStrictDerivAt_exp exp_ne_zero

Premises used: Complex.exp_ne_zero, Complex.hasStrictDerivAt_exp, isOpenMap_of_hasStrictDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
x : ℂ
h : x ∈ slitPlane
h0 : x ≠ 0
⊢ HasStrictDerivAt (↑expOpenPartialHomeomorph : ℂ → ℂ) x ((↑expOpenPartialHomeomorph.symm : ℂ → ℂ) x)

Tactic:
simpa [exp_log h0] using hasStrictDerivAt_exp (log x)

Premises used: Complex.log, Complex.hasStrictDerivAt_exp, Complex.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ HasDerivAt log z⁻¹ z

Tactic:
HasStrictDerivAt.hasDerivAt <| hasStrictDerivAt_log hz

Premises used: Complex.hasStrictDerivAt_log, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ DifferentiableAt ℂ log z

Tactic:
(hasDerivAt_log hz).differentiableAt

Premises used: HasDerivAt.differentiableAt, Complex.hasDerivAt_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
x : ℂ
h : x ∈ slitPlane
⊢ HasStrictFDerivAt log (HSMul.hSMul (β := ℂ →L[ℝ] ℂ) x⁻¹ 1) x

Tactic:
(hasStrictDerivAt_log h).complexToReal_fderiv

Premises used: Complex.hasStrictDerivAt_log, HasStrictDerivAt.complexToReal_fderiv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
x : ℂ
h : x ∈ slitPlane
n : WithTop ℕ∞
⊢ ContDiffAt ℂ n log x

Tactic:
expOpenPartialHomeomorph.contDiffAt_symm_deriv (exp_ne_zero <| log x) h (hasDerivAt_exp _)
    contDiff_exp.contDiffAt

Premises used: Complex.log, OpenPartialHomeomorph.contDiffAt_symm_deriv, Complex.exp_ne_zero, OpenPartialHomeomorph.toFun', Complex.contDiff_exp, Complex.expOpenPartialHomeomorph, Complex.hasDerivAt_exp, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
h₁ : HasStrictFDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictFDerivAt (fun (t : E) ↦ log (f t)) ((f x)⁻¹ • f') x

Tactic:
(hasStrictDerivAt_log h₂).comp_hasStrictFDerivAt x h₁

Premises used: Complex.log, Complex.hasStrictDerivAt_log, HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
rw : HasStrictDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x
⊢ HasStrictDerivAt (fun (t : ℂ) ↦ log (f t)) (f' / f x) x

Tactic:
rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x

Tactic:
(hasStrictDerivAt_log h₂).comp x h₁

Premises used: Complex.log, Complex.hasStrictDerivAt_log, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x

Tactic:
exact (hasStrictDerivAt_log h₂).comp x h₁

Premises used: Complex.hasStrictDerivAt_log, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun (t : ℝ) ↦ log (f t)) (f' / f x) x

Tactic:
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).comp_hasStrictDerivAt x h₁

Premises used: HasStrictFDerivAt.comp_hasStrictDerivAt, Complex.hasStrictFDerivAt_log_real, div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
h₁ : HasFDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasFDerivAt (fun (t : E) ↦ log (f t)) ((f x)⁻¹ • f') x

Tactic:
(hasStrictDerivAt_log h₂).hasDerivAt.comp_hasFDerivAt x h₁

Premises used: Complex.log, Complex.hasStrictDerivAt_log, HasStrictDerivAt.hasDerivAt, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
rw : HasDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x
⊢ HasDerivAt (fun (t : ℂ) ↦ log (f t)) (f' / f x) x

Tactic:
rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x

Tactic:
(hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁

Premises used: Complex.log, HasDerivAt.comp, Complex.hasStrictDerivAt_log, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') x

Tactic:
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁

Premises used: HasDerivAt.comp, Complex.hasStrictDerivAt_log, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasDerivAt f f' x
h₂ : f x ∈ slitPlane
⊢ HasDerivAt (fun (t : ℝ) ↦ log (f t)) (f' / f x) x

Tactic:
simpa only [div_eq_inv_mul] using
    (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivAt x h₁

Premises used: HasFDerivAt.comp_hasDerivAt, HasStrictFDerivAt.hasFDerivAt, Complex.hasStrictFDerivAt_log_real, div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
⊢ DifferentiableAt ℂ (F := ℂ) (fun (t : E) ↦ log (f t)) x

Tactic:
(h₁.hasFDerivAt.clog h₂).differentiableAt

Premises used: HasFDerivAt.clog, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
s : Set E
x : E
h₁ : HasFDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasFDerivWithinAt (fun (t : E) ↦ log (f t)) ((f x)⁻¹ • f') s x

Tactic:
(hasStrictDerivAt_log h₂).hasDerivAt.comp_hasFDerivWithinAt x h₁

Premises used: Complex.log, HasDerivAt.comp_hasFDerivWithinAt, Complex.hasStrictDerivAt_log, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
rw : HasDerivWithinAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') s x
⊢ HasDerivWithinAt (fun (t : ℂ) ↦ log (f t)) (f' / f x) s x

Tactic:
rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') s x

Tactic:
(hasStrictDerivAt_log h₂).hasDerivAt.comp_hasDerivWithinAt x h₁

Premises used: Complex.log, Complex.hasStrictDerivAt_log, HasDerivAt.comp_hasDerivWithinAt, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun (t : ℂ) ↦ log (f t)) ((f x)⁻¹ * f') s x

Tactic:
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp_hasDerivWithinAt x h₁

Premises used: Complex.hasStrictDerivAt_log, HasDerivAt.comp_hasDerivWithinAt, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℝ → ℂ
s : Set ℝ
x : ℝ
f' : ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun (t : ℝ) ↦ log (f t)) (f' / f x) s x

Tactic:
simpa only [div_eq_inv_mul] using
    (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivWithinAt x h₁

Premises used: HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.comp_hasDerivWithinAt, Complex.hasStrictFDerivAt_log_real, div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
x : E
h₁ : DifferentiableWithinAt ℂ f s x
h₂ : f x ∈ slitPlane
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (t : E) ↦ log (f t)) s x

Tactic:
(h₁.hasFDerivWithinAt.clog h₂).differentiableWithinAt

Premises used: HasFDerivWithinAt.clog, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
h₁ : DifferentiableOn ℂ f s
h₂ : ∀ x ∈ s, f x ∈ slitPlane
⊢ DifferentiableOn ℂ (F := ℂ) (fun (t : E) ↦ log (f t)) s

Tactic:
fun x hx => (h₁ x hx).clog (h₂ x hx)

Premises used: DifferentiableOn, DifferentiableWithinAt.clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
h₁ : Differentiable ℂ f
h₂ : ∀ (x : E), f x ∈ slitPlane
⊢ Differentiable ℂ (F := ℂ) fun (t : E) ↦ log (f t)

Tactic:
fun x =>
  (h₁ x).clog (h₂ x)

Premises used: Differentiable, DifferentiableAt.clog
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
⊢ deriv (fun (t : ℂ) ↦ log (f t)) x = deriv f x / f x

Tactic:
have A := (HasDerivAt.clog h₁.hasDerivAt h₂).deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
A : deriv (fun (t : ℂ) ↦ log (f t)) x = deriv f x / f x
⊢ deriv (fun (t : ℂ) ↦ log (f t)) x = deriv f x / f x

Tactic:
rw [← h₁.hasDerivAt.deriv] at A

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
f : ℂ → ℂ
x : ℂ
h₁ : DifferentiableAt ℂ f x
h₂ : f x ∈ slitPlane
A : deriv (fun (t : ℂ) ↦ log (f t)) x = deriv f x / f x
⊢ deriv (log ∘ f) x = logDeriv f x

Tactic:
simp only [logDeriv, Pi.div_apply, ← A, Function.comp_def]

Premises used: logDeriv, Pi.div_apply, Function.comp_def
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
𝕜 : Type u_3
𝕜' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : CompleteSpace 𝕜'
f : 𝕜 → 𝕜'
s : Set 𝕜
h : MeromorphicOn f s
⊢ MeromorphicOn (logDeriv f) s

Tactic:
h.deriv.div h

Premises used: MeromorphicOn.deriv, logDeriv, MeromorphicOn.div
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Goal:
𝕜 : Type u_3
𝕜' : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
inst_3 : CompleteSpace 𝕜'
f : 𝕜 → 𝕜'
h : Meromorphic f
⊢ Meromorphic (logDeriv f)

Tactic:
h.deriv.div h

Premises used: logDeriv, Meromorphic.deriv, Meromorphic.div
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
a : A
⊢ abs (-a) = abs a

Tactic:
simp [abs]

Premises used: CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
a : A
⊢ 0 ≤ abs a

Tactic:
sqrt_nonneg _

Premises used: CFC.sqrt_nonneg, CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
a : A
ha : IsStarNormal a
⊢ abs (star a) = abs a

Tactic:
simp [abs, star_comm_self']

Premises used: star_comm_self', CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
⊢ abs 0 = 0

Tactic:
simp [abs]

Premises used: CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
⊢ abs a * abs a = star a * a

Tactic:
sqrt_mul_sqrt_self _ <| star_mul_self_nonneg _

Premises used: star_mul_self_nonneg, CFC.abs, CFC.sqrt_mul_sqrt_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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)
⊢ Commute (star a * a) b

Tactic:
simp_all [h₂.star_left]

Premises used: Commute.star_left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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)
⊢ Commute b (abs a)

Tactic:
h₁.cfcAbs_left h₂ |>.symm

Premises used: Commute.symm, Commute.cfcAbs_left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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)
⊢ Commute (star a * a) (star b * b)

Tactic:
simp_all [h₂.star_left]

Premises used: Commute.star_left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
⊢ Commute (abs a) a

Tactic:
.cfcAbs_left (.refl a) ha.star_comm_self.symm

Premises used: IsStarNormal.star_comm_self, Commute.symm, Commute.refl, Commute.cfcAbs_left
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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)
⊢ Commute (abs a) (abs b)

Tactic:
have hab := h₁.cfcAbs_cfcAbs h₂
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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)
rw₈ rw₉ : star b * star a * (b * a) = star b * star a * (b * a)
⊢ abs (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]

Premises used: Commute.mul_mul_mul_comm, Commute.mul_nonneg, CFC.abs_nonneg, CFC.sqrt_eq_iff, Commute.symm, StarMul.star_mul, CFC.abs, CFC.abs_mul_abs, Commute.star_left, Commute.eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
rw₁ rw₂ : star a * a = star a * a
⊢ abs (a * a) = star a * a

Tactic:
rw [Commute.cfcAbs_mul_eq (.refl a) ha.star_comm_self.symm, abs_mul_abs]

Premises used: IsStarNormal.star_comm_self, Commute.cfcAbs_mul_eq, Commute.symm, Commute.refl, CFC.abs_mul_abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
simp : abs a * abs a = star a * a
⊢ HPow.hPow (β := ℝ≥0) (abs a) 2 = star a * a

Tactic:
simp only [abs_nonneg, nnrpow_two]

Premises used: CFC.abs_nonneg, CFC.nnrpow_two
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
⊢ abs a * abs a = star a * a

Tactic:
apply abs_mul_abs

Premises used: CFC.abs_mul_abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
rw₁ rw₂ : (star a * a) ^ x = (star a * a) ^ x
⊢ abs a ^ (2 * x) = (star a * a) ^ x

Tactic:
rw [← nnrpow_nnrpow, abs_nnrpow_two]

Premises used: CFC.abs_nnrpow_two, CFC.nnrpow_nnrpow
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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 ^ x = (star a * a) ^ (x / 2)

Tactic:
simp only [← abs_nnrpow_two_mul, mul_div_left_comm, ne_eq, OfNat.ofNat_ne_zero,
    not_false_eq_true, div_self, mul_one]

Premises used: OfNat.ofNat_ne_zero, CFC.abs_nnrpow_two_mul, ne_eq, mul_one, not_false_eq_true, mul_div_left_comm, div_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
rw₂ rw₃ : a = a
⊢ abs a = a

Tactic:
rw [abs, ha.star_eq, sqrt_mul_self a ha]

Premises used: LE.le.star_eq, CFC.abs, CFC.sqrt_mul_self
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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 : a ≤ 0
⊢ abs a = -a

Tactic:
simpa using abs_of_nonneg (-a)

Premises used: CFC.abs_of_nonneg, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(x * x)) a
| abs a

Tactic:
rw [abs, ha.star_eq, sqrt_eq_real_sqrt .., ← cfcₙ_id' ℝ a, ← cfcₙ_mul .., ← cfcₙ_comp' ..]

Premises used: Real, cfcₙ_id', cfcₙ_mul, cfcₙ_comp', CFC.abs, CFC.sqrt_eq_real_sqrt, IsSelfAdjoint.star_eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
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
conv_lhs : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(x * x)) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
⊢ abs 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' ..]

Premises used: Real, cfcₙ_id', cfcₙ_mul, cfcₙ_comp', CFC.abs, CFC.sqrt_eq_real_sqrt, IsSelfAdjoint.star_eq