awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ √(x * x)) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a

Tactic:
simp [← sq, Real.sqrt_sq_eq_abs]

Premises used: Real.sqrt_sq_eq_abs, sq
-- 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 = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
⊢ a⁺ + a⁻ = abs a

Tactic:
rw [CFC.posPart_def, CFC.negPart_def, ← cfcₙ_add .., abs_eq_cfcₙ_norm a ha]

Premises used: cfcₙ_add, CFC.abs_eq_cfcₙ_norm, CFC.negPart_def, CFC.posPart_def
-- 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
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ + x⁻) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a

Tactic:
cfcₙ_congr fun x hx ↦ posPart_add_negPart x

Premises used: cfcₙ_congr, posPart_add_negPart
-- 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
⊢ cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ x⁺ + x⁻) a = cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a

Tactic:
exact cfcₙ_congr fun x hx ↦ posPart_add_negPart x

Premises used: cfcₙ_congr, posPart_add_negPart
-- 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
⊢ abs a - a = HSMul.hSMul (α := ℕ) 2 a⁻

Tactic:
simpa [two_smul] using
    congr($(CFC.posPart_add_negPart a) - $(CFC.posPart_sub_negPart a)).symm

Premises used: congrArg, CFC.posPart_sub_negPart, HSub.hSub, two_smul, id, CFC.posPart_add_negPart, congr, Eq.symm
-- 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
⊢ abs a + a = HSMul.hSMul (α := ℕ) 2 a⁺

Tactic:
simpa [two_smul] using
    congr($(CFC.posPart_add_negPart a) + $(CFC.posPart_sub_negPart a)).symm

Premises used: congrArg, CFC.posPart_sub_negPart, two_smul, id, CFC.posPart_add_negPart, HAdd.hAdd, congr, Eq.symm
-- 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 (abs a) = abs a

Tactic:
abs_of_nonneg ..

Premises used: CFC.abs_of_nonneg
-- 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
inst_12 : StarModule ℝ A
R : Type u_3
inst_13 : Semiring R
inst_14 : SMulWithZero R ℝ≥0
inst_15 : SMul R A
inst_16 : IsScalarTower R ℝ≥0 A
r : R
a : A
this : ∀ (r : ℝ≥0), abs (r • a) = r • abs a
⊢ abs (r • a) = r • abs a

Tactic:
simpa using this (r • 1)

Premises used: HSMul.hSMul, OfNat.ofNat
-- 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
inst_12 : StarModule ℝ A
R : Type u_3
inst_13 : Semiring R
inst_14 : SMulWithZero R ℝ≥0
inst_15 : SMul R A
inst_16 : IsScalarTower R ℝ≥0 A
r : R
a : A
suffices : ∀ (r : ℝ≥0), abs (r • a) = r • abs a
⊢ abs (r • a) = r • abs a

Tactic:
suffices ∀ r : ℝ≥0, abs (r • a) = r • abs a by simpa using this (r • 1)
-- 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
inst_12 : StarModule ℝ A
R : Type u_3
inst_13 : Semiring R
inst_14 : SMulWithZero R ℝ≥0
inst_15 : SMul R A
inst_16 : IsScalarTower R ℝ≥0 A
r_1 : R
a : A
r : ℝ≥0
⊢ 0 ≤ r

Tactic:
positivity
-- 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
inst_12 : StarModule ℝ A
R : Type u_3
inst_13 : Semiring R
inst_14 : SMulWithZero R ℝ≥0
inst_15 : SMul R A
inst_16 : IsScalarTower R ℝ≥0 A
r_1 : R
a : A
r : ℝ≥0
rw : r • abs a * r • abs a = star (r • a) * r • a
⊢ abs (r • a) = r • abs a

Tactic:
rw [abs, sqrt_eq_iff _ _ (star_mul_self_nonneg _) (smul_nonneg (by positivity) (abs_nonneg _))]

Premises used: smul_nonneg, CFC.abs_nonneg, CFC.sqrt_eq_iff, 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
inst_12 : StarModule ℝ A
R : Type u_3
inst_13 : Semiring R
inst_14 : SMulWithZero R ℝ≥0
inst_15 : SMul R A
inst_16 : IsScalarTower R ℝ≥0 A
r_1 : R
a : A
r : ℝ≥0
⊢ r • abs a * r • abs a = star (r • a) * r • a

Tactic:
simp [mul_smul_comm, smul_mul_assoc, abs_mul_abs]

Premises used: smul_mul_assoc, mul_smul_comm, CFC.abs_mul_abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
⊢ 0 ≤ cfcₙ (p := p) (fun (z : 𝕜) ↦ star (f z) * f z) a

Tactic:
cfcₙ_nonneg fun _ _ ↦ star_mul_self_nonneg _

Premises used: star_mul_self_nonneg, cfcₙ_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
h : x ∈ quasispectrum 𝕜 a
⊢ LE.le.{u_1} (α := 𝕜) 0 (↑‖f x‖ : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
trans : abs (r • a) = abs (‖r‖ • a)
trans₁ : abs (‖r‖ • a) = ‖r‖ • abs a
⊢ abs (r • a) = ‖r‖ • abs a

Tactic:
trans abs (‖r‖ • a)

Premises used: Norm.norm, HSMul.hSMul, CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
simp :
  sqrt ((r • star r) • (star a * a)) = sqrt (HSMul.hSMul (α := 𝕜) (β := 𝕜) (↑‖r‖ : 𝕜) (star (↑‖r‖ : 𝕜)) • (star a * a))
⊢ abs (r • a) = abs (‖r‖ • a)

Tactic:
simp only [abs, mul_smul_comm, smul_mul_assoc, star_smul, ← smul_assoc,
      RCLike.real_smul_eq_coe_smul (K := 𝕜)]

Premises used: smul_assoc, StarModule.star_smul, RCLike.real_smul_eq_coe_smul, smul_mul_assoc, mul_smul_comm, CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ sqrt ((r • star r) • (star a * a)) = sqrt (HSMul.hSMul (α := 𝕜) (β := 𝕜) (↑‖r‖ : 𝕜) (star (↑‖r‖ : 𝕜)) • (star a * a))

Tactic:
simp [-algebraMap_smul, ← smul_mul_assoc, ← mul_comm (starRingEnd _ _), RCLike.conj_mul, sq]

Premises used: RCLike.conj_mul, smul_mul_assoc, algebraMap_smul, sq, mul_comm, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
⊢ 0 ≤ ‖r‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r : 𝕜
a : A
lift : ∀ (r : ℝ≥0), abs ((↑r : ℝ) • a) = (↑r : ℝ) • abs a
⊢ abs (‖r‖ • a) = ‖r‖ • abs a

Tactic:
lift ‖r‖ to ℝ≥0 using norm_nonneg _ with r

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : Module ℝ A
inst_10 : SMulCommClass ℝ A A
inst_11 : IsScalarTower ℝ A A
inst_12 : NonnegSpectrumClass ℝ A
inst_13 : IsTopologicalRing A
inst_14 : T2Space A
inst_15 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_16 : StarModule 𝕜 A
inst_17 : StarModule ℝ A
inst_18 : IsScalarTower ℝ 𝕜 A
r_1 : 𝕜
a : A
r : ℝ≥0
⊢ abs ((↑r : ℝ) • a) = (↑r : ℝ) • abs a

Tactic:
simp [← NNReal.smul_def]

Premises used: NNReal.smul_def
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
rw : cfcₙ (p := p) (fun (x : 𝕜) ↦ HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖x‖ : 𝕜)) a = star a * a
⊢ abs a = cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a

Tactic:
rw [abs, sqrt_eq_iff _ _ (hb := cfcₙ_norm_nonneg _ _), ← cfcₙ_mul ..]

Premises used: cfcₙ_norm_nonneg, CFC.sqrt_eq_iff, cfcₙ_mul, CFC.abs
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
rw : cfcₙ (p := p) (fun (x : 𝕜) ↦ star x * x) a
| star a * a

Tactic:
rw [← cfcₙ_id' 𝕜 a, ← cfcₙ_star, ← cfcₙ_mul ..]

Premises used: cfcₙ_id', cfcₙ_mul, cfcₙ_star
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
conv_rhs :
  cfcₙ (p := p) (fun (x : 𝕜) ↦ HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) (fun (x : 𝕜) ↦ star x * x) a
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖x‖ : 𝕜)) a = star a * a

Tactic:
conv_rhs => rw [← cfcₙ_id' 𝕜 a, ← cfcₙ_star, ← cfcₙ_mul ..]

Premises used: cfcₙ_id', cfcₙ_mul, cfcₙ_star
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ HMul.hMul (α := 𝕜) (↑‖x‖ : 𝕜) (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) (fun (x : 𝕜) ↦ star x * x) a

Tactic:
simp [RCLike.conj_mul, sq]

Premises used: RCLike.conj_mul, sq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
inl : ∀ (hf0 : f 0 = 0), cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
inr : ∀ (hf0 : ¬f 0 = 0), cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)

Tactic:
obtain (hf0 | hf0) := em (f 0 = 0)

Premises used: em, OfNat.ofNat, Eq
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
hf0 : f 0 = 0
inl : cfcₙ (p := p) f (cfcₙ (p := p) (fun (x : 𝕜) ↦ (↑‖x‖ : 𝕜)) a) = cfcₙ (p := p) f (abs a)
inl₁ inl₂ : cfcₙ (p := p) f (abs a) = cfcₙ (p := p) f (abs a)
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)

Tactic:
rw [cfcₙ_comp' f (‖·‖) a, ← abs_eq_cfcₙ_coe_norm _ a]

Premises used: Norm.norm, CFC.abs_eq_cfcₙ_coe_norm, RCLike.ofReal, cfcₙ_comp'
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
hf0 : ¬f 0 = 0
h : f (↑(norm.{u_1} (E := 𝕜) 0) : 𝕜) = 0
⊢ f 0 = 0

Tactic:
simpa using h
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
f : 𝕜 → 𝕜
a : A
ha : p a
hf : ContinuousOn f ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
hf0 : ¬f 0 = 0
inr : cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = 0
inr₁ inr₂ : Eq.{u_2 + 1} (α := A) 0 0
⊢ cfcₙ (p := p) (fun (x : 𝕜) ↦ f (↑‖x‖ : 𝕜)) a = cfcₙ (p := p) f (abs a)

Tactic:
rw [cfcₙ_apply_of_not_map_zero _ hf0,
      cfcₙ_apply_of_not_map_zero _ (fun h ↦ (hf0 <| by simpa using h).elim)]

Premises used: False.elim, cfcₙ_apply_of_not_map_zero
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
𝕜 : Type u_1
A : Type u_2
p : A → Prop
inst : RCLike 𝕜
inst_1 : NonUnitalRing A
inst_2 : TopologicalSpace A
inst_3 : Module 𝕜 A
inst_4 : StarRing A
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : IsScalarTower 𝕜 A A
inst_8 : SMulCommClass 𝕜 A A
inst_9 : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst_10 : Module ℝ A
inst_11 : SMulCommClass ℝ A A
inst_12 : IsScalarTower ℝ A A
inst_13 : NonnegSpectrumClass ℝ A
inst_14 : IsTopologicalRing A
inst_15 : T2Space A
inst_16 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : p a
rw : quasispectrum 𝕜 (cfcₙ (p := p) (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a
rw₁ rw₂ :
  Eq (α := Set 𝕜) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a) ((fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a)
⊢ quasispectrum 𝕜 (abs a) = (fun (z : 𝕜) ↦ (↑‖z‖ : 𝕜)) '' quasispectrum 𝕜 a

Tactic:
rw [abs_eq_cfcₙ_coe_norm 𝕜 a ha, cfcₙ_map_quasispectrum ..]

Premises used: CFC.abs_eq_cfcₙ_coe_norm, cfcₙ_map_quasispectrum
-- Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Goal:
A : Type u_2
inst : Ring A
inst_1 : StarRing A
inst_2 : TopologicalSpace A
inst_3 : Algebra ℝ A
inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_5 : PartialOrder A
inst_6 : StarOrderedRing A
inst_7 : NonnegSpectrumClass ℝ A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
a : A
ha : IsSelfAdjoint a
rw : cfcₙ (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
rw₁ rw₂ : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a
⊢ abs a = cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ ‖x‖) a

Tactic:
rw [abs_eq_cfcₙ_norm _, cfcₙ_eq_cfc]

Premises used: cfcₙ_eq_cfc, CFC.abs_eq_cfcₙ_norm