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 : CommRing R
inst_1 : PartialOrder R
inst_2 : Nontrivial R
inst_3 : StarRing R
inst_4 : MetricSpace R
inst_5 : IsTopologicalRing R
inst_6 : ContinuousStar R
inst_7 : ContinuousSqrt R
inst_8 : StarOrderedRing R
inst_9 : NoZeroDivisors R
inst_10 : TopologicalSpace A
inst_11 : NonUnitalRing A
inst_12 : StarRing A
inst_13 : PartialOrder A
inst_14 : StarOrderedRing A
inst_15 : Module R A
inst_16 : IsScalarTower R A A
inst_17 : SMulCommClass R A A
inst_18 : NonUnitalContinuousFunctionalCalculus R A p
inst_19 : NonnegSpectrumClass R A
f : R → R
a : A
hf : ContinuousOn f (σₙ R a)
h0 : f 0 = 0
ha : p a
⊢ 0 ≤ cfcₙ (p := p) (fun (x : R) ↦ -f x) a ↔ ∀ x ∈ σₙ R a, 0 ≤ -f x

Tactic:
exact cfcₙ_nonneg_iff (fun x ↦ -f x) a

Premises used: cfcₙ_nonneg_iff, Neg.neg
-- 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
ha : p a
s : Set R
hs : σₙ R a ⊆ s
⊢ Continuous[_, inst_8]
    (⇑(cfcₙHomSuperset (p := p) ha (s := s) hs : C((↑s : Type u_1), R)₀ →⋆ₙₐ[R] A) : (a : C((↑s : Type u_1), R)₀) → A)

Tactic:
have : Fact (0 ∈ s) := ⟨hs (quasispectrum.zero_mem R a)⟩
  (cfcₙHom_continuous ha).comp <| ContinuousMapZero.continuous_precomp _

Premises used: Subtype.map, ContinuousMap.mk, Continuous.comp, quasispectrum.zero_mem, id, Fact.mk, cfcₙHom_continuous, ContinuousMapZero.mk, ContinuousMapZero.continuous_precomp, cfcₙHomSuperset._proof_2, cfcₙHomSuperset._proof_3
-- 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
ha : p a
s : Set R
hs : σₙ R a ⊆ s
⊢ ((cfcₙHomSuperset (p := p) ha (s := s) hs : C((↑s : Type u_1), R)₀ →⋆ₙₐ[R] A) : (a : C((↑s : Type u_1), R)₀) → A)
      (ContinuousMapZero.id s) =
    a

Tactic:
cfcₙHom_id ha

Premises used: Set.Mem, cfcₙHom_id, setOf, quasispectrum, ContinuousMap.comp, ContinuousMapZero.id, ContinuousMapZero.comp, ContinuousMap.restrict
-- 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 : NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding a ha

Premises used: NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ Continuous (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := C((↑(σₙ R a) : Type u_1), R))
    (⇑(↑(NonUnitalStarAlgHom.toNonUnitalAlgHom toContinuousMapHom) :
          C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(σₙ R a) : Type u_1), R)) :
      (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(cfcₙHom_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
(cfcHom_injective ha).comp fun f g h ↦ ?_

Premises used: cfcHom_injective, Function.Injective.comp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
refine :
  ∀ (f g : C((↑(σₙ R a) : Type u_1), R)₀)
    (h :
      Eq (α := C((↑(spectrum R a) : Type u_1), R))
        (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                    (NonUnitalStarAlgHom.comp
                      (↑(compStarAlgHom' R R
                            { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                        C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                      toContinuousMapHom)) :
                C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
              (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
            f :
          C((↑(spectrum R a) : Type u_1), R))
        (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                    (NonUnitalStarAlgHom.comp
                      (↑(compStarAlgHom' R R
                            { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                        C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                      toContinuousMapHom)) :
                C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
              (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
            g :
          C((↑(spectrum R a) : Type u_1), R))),
    f = g
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := C((↑(σₙ R a) : Type u_1), R)₀) (β := A)
    (⇑(cfcₙHom_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
refine (cfcHom_injective ha).comp fun f g h ↦ ?_

Premises used: cfcHom_injective, Function.Injective.comp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
h₁ :
  ∀ (x : (↑(σₙ R a) : Type u_1)),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
h₁ : Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R)
h₂ :
  ∀ (hx : x ≠ 0),
    Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
hx : x ≠ 0
⊢ (↑x : R) = 0 ∨ (↑x : R) ∈ spectrum R a

Tactic:
simpa [quasispectrum_eq_spectrum_union_zero] using x.prop

Premises used: Subtype.prop, quasispectrum_eq_spectrum_union_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
hx : x ≠ 0
⊢ (↑x : R) = 0 ∨ (↑x : R) ∈ spectrum R a

Tactic:
have := by simpa [quasispectrum_eq_spectrum_union_zero] using x.prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
hx : x ≠ 0
this : (↑x : R) = 0 ∨ (↑x : R) ∈ spectrum R a
⊢ (↑x : R) ∈ spectrum R a

Tactic:
replace := this.resolve_left (Subtype.val_injective.ne_iff.mpr hx)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f g : C((↑(σₙ R a) : Type u_1), R)₀
h :
  Eq (α := C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        f :
      C((↑(spectrum R a) : Type u_1), R))
    (((↑(NonUnitalStarAlgHom.toNonUnitalAlgHom
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom)) :
            C((↑(σₙ R a) : Type u_1), R)₀ →ₙ* C((↑(spectrum R a) : Type u_1), R)) :
          (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(spectrum R a) : Type u_1), R))
        g :
      C((↑(spectrum R a) : Type u_1), R))
x : (↑(σₙ R a) : Type u_1)
hx : x ≠ 0
this : (↑x : R) ∈ spectrum R a
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) ((g : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)

Tactic:
congrm($h ⟨x, this⟩)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
simp :
  quasispectrum.{u_1, u_2} R (A := A)
      ((NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →⋆ₙₐ[R] A)
              (NonUnitalStarAlgHom.comp
                (↑(compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ :
                        C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) }) :
                  C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                toContinuousMapHom) :
            (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          f :
        A) =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
⊢ quasispectrum.{u_1, u_2} R (A := A)
      ((cfcₙHom_of_cfcHom R (p := p) ha : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A) f : A) =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)

Tactic:
simp only [cfcₙHom_of_cfcHom]

Premises used: cfcₙHom_of_cfcHom
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
ha : p a
f : C((↑(σₙ R a) : Type u_1), R)₀
rw :
  spectrum.{u_1, u_2} R (A := A)
        ((NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →⋆ₙₐ[R] A)
                (NonUnitalStarAlgHom.comp
                  (↑(compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ :
                          C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) }) :
                    C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                  toContinuousMapHom) :
              (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
            f :
          A) ∪
      {0} =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
⊢ quasispectrum.{u_1, u_2} R (A := A)
      ((NonUnitalStarAlgHom.comp (↑(cfcHom (p := p) ha) : C((↑(spectrum R a) : Type u_1), R) →⋆ₙₐ[R] A)
              (NonUnitalStarAlgHom.comp
                (↑(compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ :
                        C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) }) :
                  C((↑(σₙ R a) : Type u_1), R) →⋆ₙₐ[R] C((↑(spectrum R a) : Type u_1), R))
                toContinuousMapHom) :
            (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
          f :
        A) =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)

Tactic:
rw [quasispectrum_eq_spectrum_union_zero]

Premises used: quasispectrum_eq_spectrum_union_zero