awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
h_spec : σₙ R a ⊆ {0}
ha : p a
x : R
⊢ x ∈ σₙ R a → id x = (fun (x : R) ↦ (0 : R)) x

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
a : A
h_spec : σₙ R a ⊆ {0}
ha : p a
⊢ a = 0

Tactic:
simpa [cfcₙ_id R a] using cfcₙ_congr (a := a) (f := id) (g := fun _ : R ↦ 0) fun x ↦ by simp_all

Premises used: cfcₙ_id, cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
⊢ quasispectrum.{u_1, u_2} R (A := A) 0 = {0}

Tactic:
Set.eq_singleton_iff_unique_mem.mpr ⟨quasispectrum.zero_mem R 0, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, quasispectrum.zero_mem, And.intro, Set.eq_singleton_iff_unique_mem, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
refine : ∀ (x : R) (hx : x ∈ quasispectrum.{u_1, u_2} R (A := A) 0), x = 0
⊢ quasispectrum.{u_1, u_2} R (A := A) 0 = {0}

Tactic:
refine Set.eq_singleton_iff_unique_mem.mpr ⟨quasispectrum.zero_mem R 0, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, quasispectrum.zero_mem, And.intro, Set.eq_singleton_iff_unique_mem, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
x : R
hx : x ∈ σₙ R (cfcₙ.{u_1, u_2} (R := R) (p := p) 0 0)
⊢ ContinuousOn (Y := R) 0 (quasispectrum.{u_1, u_2} R (A := A) 0)

Tactic:
cfc_cont_tac
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
x : R
hx : x ∈ σₙ R (cfcₙ.{u_1, u_2} (R := R) (p := p) 0 0)
⊢ Eq.{u_1 + 1} (α := R) (0 0) 0

Tactic:
cfc_zero_tac
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
x : R
hx : x ∈ quasispectrum.{u_1, u_2} R (A := A) 0
⊢ Membership.mem (γ := Set R) (0 '' quasispectrum.{u_1, u_2} R (A := A) 0) x

Tactic:
rw [← cfcₙ_zero R (0 : A),
    cfcₙ_map_quasispectrum _ _ (by cfc_cont_tac) (by cfc_zero_tac) (cfcₙ_predicate_zero R)] at hx

Premises used: cfcₙ_zero, cfcₙ_predicate_zero, OfNat.ofNat, cfcₙ_map_quasispectrum
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
x : R
hx : Membership.mem (γ := Set R) (0 '' quasispectrum.{u_1, u_2} R (A := A) 0) x
⊢ x = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
pos : ∀ (hf0 : f 0 = 0), cfcₙ (p := p) f 0 = 0
neg : ∀ (hf0 : ¬f 0 = 0), cfcₙ (p := p) f 0 = 0
⊢ cfcₙ (p := p) f 0 = 0

Tactic:
by_cases hf0 : f 0 = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
hf0 : f 0 = 0
pos : cfcₙ (p := p) f 0 = cfcₙ.{u_1, u_2} (R := R) (p := p) 0 0
⊢ cfcₙ (p := p) f 0 = 0

Tactic:
nth_rw 2 [← cfcₙ_zero R 0]

Premises used: cfcₙ_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
hf0 : f 0 = 0
pos : Set.EqOn f 0 (quasispectrum.{u_1, u_2} R (A := A) 0)
⊢ cfcₙ (p := p) f 0 = cfcₙ.{u_1, u_2} (R := R) (p := p) 0 0

Tactic:
apply cfcₙ_congr

Premises used: cfcₙ_congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
hf0 : f 0 = 0
⊢ Set.EqOn f 0 (quasispectrum.{u_1, u_2} R (A := A) 0)

Tactic:
simpa [CFC.quasispectrum_zero_eq]

Premises used: CFC.quasispectrum_zero_eq
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
hf0 : ¬f 0 = 0
⊢ cfcₙ (p := p) f 0 = 0

Tactic:
cfcₙ_apply_of_not_map_zero _ hf0

Premises used: cfcₙ_apply_of_not_map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
hf0 : ¬f 0 = 0
⊢ cfcₙ (p := p) f 0 = 0

Tactic:
exact cfcₙ_apply_of_not_map_zero _ hf0

Premises used: cfcₙ_apply_of_not_map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
⊢ Commute (star (cfcₙ (p := p) f a)) (cfcₙ (p := p) f a)

Tactic:
cfcₙ_cases (fun x ↦ Commute (star x) x) _ _ (Commute.zero_right _) fun _ _ _ ↦ ?_

Premises used: Commute, Commute.zero_right, cfcₙ_cases, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
refine :
  ∀ (x : ContinuousOn f (σₙ R a))
    (x_1 :
      Eq (α := R)
        (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
                C((↑(σₙ R a) : Type u_1), R) } :
              (a : (↑(σₙ R a) : Type u_1)) → R)
            0 :
          R)
        (0 : R))
    (x_2 : p a),
    (fun (x : A) ↦ Commute (star x) x)
      ((cfcₙHom (p := p) x_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := x_1 :
          C((↑(σₙ R a) : Type u_1), R)₀ })
⊢ Commute (star (cfcₙ (p := p) f a)) (cfcₙ (p := p) f a)

Tactic:
refine cfcₙ_cases (fun x ↦ Commute (star x) x) _ _ (Commute.zero_right _) fun _ _ _ ↦ ?_

Premises used: Commute, Commute.zero_right, cfcₙ_cases, Star.star
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
h : ContinuousOn f (σₙ R a)
h_1 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h_2 : p a
rw : cfcₙ (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfcₙ (p := p) (fun (x : R) ↦ f x * star (f x)) a
⊢ HMul.hMul (α := A) (β := A)
      (star
          ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
            { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
              C((↑(σₙ R a) : Type u_1), R)₀ }) :
        A)
      ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A) =
    HMul.hMul (α := A) (β := A)
      ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
            C((↑(σₙ R a) : Type u_1), R)₀ } :
        A)
      (star
          ((cfcₙHom (p := p) h_2 : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
            { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := h_1 :
              C((↑(σₙ R a) : Type u_1), R)₀ }) :
        A)

Tactic:
rw [← cfcₙ_apply f a, ← cfcₙ_star, ← cfcₙ_mul .., ← cfcₙ_mul ..]

Premises used: cfcₙ_mul, cfcₙ_star, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
h_1 : ContinuousOn f (σₙ R a)
h_2 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h_3 : p a
h : ∀ (x : R), star (f x) * f x = f x * star (f x)
⊢ cfcₙ (p := p) (fun (x : R) ↦ star (f x) * f x) a = cfcₙ (p := p) (fun (x : R) ↦ f x * star (f x)) a

Tactic:
congr! 2
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
h : ContinuousOn f (σₙ R a)
h_1 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h_2 : p a
x : R
⊢ star (f x) * f x = f x * star (f x)

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p
f_1 g : R → R
a_1 : A
hf : ContinuousOn f_1 (σₙ R a_1)
hf0 : f_1 0 = 0
hg : ContinuousOn g (σₙ R a_1)
hg0 : g 0 = 0
ha : p a_1
f : R → R
a : A
h : ContinuousOn f (σₙ R a)
h_1 :
  Eq (α := R)
    (({ toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ : C((↑(σₙ R a) : Type u_1), R) } :
          (a : (↑(σₙ R a) : Type u_1)) → R)
        0 :
      R)
    (0 : R)
h_2 : p a
x : R
⊢ star (f x) * f x = f x * star (f x)

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A IsSelfAdjoint
f : R → R
a : A
⊢ IsSelfAdjoint (cfcₙ (p := IsSelfAdjoint) f a)

Tactic:
cfcₙ_predicate _ _

Premises used: cfcₙ_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : LE A
inst_13 : NonUnitalContinuousFunctionalCalculus R A fun (x : A) ↦ 0 ≤ x
f : R → R
a : A
⊢ 0 ≤ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a

Tactic:
cfcₙ_predicate _ _

Premises used: cfcₙ_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
pos : ∀ (ha : p a), cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a
neg : ∀ (ha : ¬p a), cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a
⊢ cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a

Tactic:
by_cases ha : p a
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
pos :
  Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x - g x, continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (HSub.hSub (α := C((↑(σₙ R a) : Type u_1), R)₀)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }) :
      A)
⊢ cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a

Tactic:
rw [cfcₙ_apply f a, cfcₙ_apply g a, ← map_sub, cfcₙ_apply ..]

Premises used: map_sub, cfcₙ_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : p a
⊢ Eq.{u_2 + 1} (α := A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) fun (x : R) ↦ f x - g x, continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
    ((cfcₙHom (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
        (HSub.hSub (α := C((↑(σₙ R a) : Type u_1), R)₀)
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }
          { toFun := (σₙ R a).restrict (π := fun (a : R) ↦ R) g, continuous_toFun := ⋯, map_zero' := ⋯ :
            C((↑(σₙ R a) : Type u_1), R)₀ }) :
      A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f g : R → R
a : A
hf : ContinuousOn f (σₙ R a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ R a)
hg0 : g 0 = 0
ha : ¬p a
⊢ cfcₙ (p := p) (fun (x : R) ↦ f x - g x) a = cfcₙ (p := p) f a - cfcₙ (p := p) g a

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Premises used: cfcₙ_apply_of_not_predicate
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
pos : ∀ (h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
neg : ∀ (h : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)), cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a
⊢ cfcₙ (p := p) (fun (x : R) ↦ -f x) a = -cfcₙ (p := p) f a

Tactic:
by_cases h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0

Premises used: quasispectrum, ContinuousOn, OfNat.ofNat
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
⊢ p a

Tactic:
obtain ⟨ha, hf, h0⟩ := h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalRing R
inst_5 : ContinuousStar R
inst_6 : TopologicalSpace A
inst_7 : NonUnitalRing A
inst_8 : StarRing A
inst_9 : Module R A
inst_10 : IsScalarTower R A A
inst_11 : SMulCommClass R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
f : R → R
a : A
h : p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0
ha : p a
⊢ ContinuousOn f (σₙ R a)

Tactic:
obtain ⟨ha, hf, h0⟩ := h