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 : 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 :
  spectrum.{u_1, u_2} R (A := A)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
            ((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)) } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          A) ∪
      {0} =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)
⊢ 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)

Tactic:
simp only [NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe]

Premises used: NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe
-- 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 :
  Eq (α := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R))
⊢ spectrum.{u_1, u_2} R (A := A)
        ((cfcHom (p := p) ha : (a : C((↑(spectrum R a) : Type u_1), R)) → A)
            ((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)) } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          A) ∪
      {0} =
    range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)

Tactic:
rw [cfcHom_map_spectrum ha]

Premises used: cfcHom_map_spectrum
-- 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)₀
h :
  ∀ (x : R),
    Membership.mem (γ := Set R)
        (range (ι := (↑(spectrum R a) : Type u_1))
            (⇑((compStarAlgHom' R R
                        { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                      (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                    ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                  C((↑(spectrum R a) : Type u_1), R)) :
              (a : (↑(spectrum R a) : Type u_1)) → R) ∪
          {0})
        x ↔
      Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x
⊢ Eq (α := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R))

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 : C((↑(σₙ R a) : Type u_1), R)₀
x : R
h :
  Membership.mem (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      x →
    Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x
h₁ :
  Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x →
    Membership.mem (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_2 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_2 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      x
⊢ Membership.mem (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      x ↔
    Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) x

Tactic:
constructor
-- 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)₀
x : (↑(spectrum R a) : Type u_1)
⊢ Membership.mem (α := R) (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R))
    ((((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
              ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
            C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        x :
      R)

Tactic:
⟨⟨x.1, spectrum_subset_quasispectrum R a x.2⟩, rfl⟩

Premises used: spectrum_subset_quasispectrum, Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range, Subtype.val, rfl, Subtype.property
-- 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)₀
x : (↑(spectrum R a) : Type u_1)
⊢ Membership.mem (α := R) (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R))
    ((((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
              ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
            C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R)
        x :
      R)

Tactic:
exact ⟨⟨x.1, spectrum_subset_quasispectrum R a x.2⟩, 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 : C((↑(σₙ R a) : Type u_1), R)₀
⊢ Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) 0

Tactic:
⟨0, map_zero f⟩

Premises used: Set.Mem, setOf, map_zero, Exists.intro, Set.range, OfNat.ofNat
-- 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)₀
⊢ Membership.mem (γ := Set R) (range (ι := (↑(σₙ R a) : Type u_1)) (⇑f : (a : (↑(σₙ R a) : Type u_1)) → R)) 0

Tactic:
exact ⟨0, map_zero f⟩
-- 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)₀
x : (↑(σₙ R a) : Type u_1)
⊢ (↑x : R) ∈ σₙ R a

Tactic:
have hx := x.2
-- 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)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) ∈ σₙ R a
⊢ (↑x : R) ∈ spectrum R a ∪ {0}

Tactic:
simp_rw [quasispectrum_eq_spectrum_union_zero R a] at hx

Premises used: 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 : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) ∈ spectrum R a ∪ {0}
h :
  ∀ (hx : (↑x : R) ∈ spectrum R a),
    Membership.mem (α := R) (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
h₁ :
  ∀ (hx : Membership.mem (γ := Set R) {0} (↑x : R)),
    Membership.mem (α := R) (γ := Set R)
      (range (ι := (↑(spectrum R a) : Type u_1))
          (⇑((compStarAlgHom' R R
                      { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                    (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                  ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
                C((↑(spectrum R a) : Type u_1), R)) :
            (a : (↑(spectrum R a) : Type u_1)) → R) ∪
        {0})
      ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)

Tactic:
obtain (hx | hx) := 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 : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) ∈ spectrum R a
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)

Tactic:
Or.inl ⟨⟨x.1, hx⟩, rfl⟩

Premises used: Set.union, Set.Mem, setOf, Subtype.mk, Exists.intro, Or.inl, Subtype.val, 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 : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) ∈ spectrum R a
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)

Tactic:
exact Or.inl ⟨⟨x.1, hx⟩, rfl⟩

Premises used: Or.inl
-- 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)₀
x : (↑(σₙ R a) : Type u_1)
hx : Membership.mem (γ := Set R) {0} (↑x : R)
h : Membership.mem (α := R) (γ := Set R) {0} ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)
⊢ Membership.mem (α := R) (γ := Set R)
    (range (ι := (↑(spectrum R a) : Type u_1))
        (⇑((compStarAlgHom' R R { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ } :
                  (a_1 : C((↑(σₙ R a) : Type u_1), R)) → C((↑(spectrum R a) : Type u_1), R))
                ((toContinuousMapHom : (a_1 : C((↑(σₙ R a) : Type u_1), R)₀) → C((↑(σₙ R a) : Type u_1), R)) f) :
              C((↑(spectrum R a) : Type u_1), R)) :
          (a : (↑(spectrum R a) : Type u_1)) → R) ∪
      {0})
    ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R)

Tactic:
apply Or.inr

Premises used: Or.inr
-- 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)₀
x : (↑(σₙ R a) : Type u_1)
hx : Membership.mem (γ := Set R) {0} (↑x : R)
⊢ (↑x : R) = 0

Tactic:
push _ ∈ _ at 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 : C((↑(σₙ R a) : Type u_1), R)₀
x : (↑(σₙ R a) : Type u_1)
hx : (↑x : R) = 0
h : Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) 0 : R) (0 : R)
h₁ h₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) ((f : (a : (↑(σₙ R a) : Type u_1)) → R) x : R) (0 : R)

Tactic:
rw [show x = 0 from Subtype.val_injective hx, map_zero]

Premises used: Subtype.val_injective, map_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 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(cfcₙHom_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
(cfcHom_isClosedEmbedding ha).comp <|
    (IsUniformInducing.isUniformEmbedding ⟨?_⟩).isClosedEmbedding

Premises used: cfcHom_isClosedEmbedding, Topology.IsClosedEmbedding.comp, IsUniformInducing.mk, IsUniformEmbedding.isClosedEmbedding, IsUniformInducing.isUniformEmbedding
-- 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 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
refine :
  Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
    (Filter.comap (β := C((↑(spectrum R a) : Type u_1), R) × C((↑(spectrum R a) : Type u_1), R))
      (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ 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))
            x.1,
          ((↑(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))
            x.2))
      (𝓤 C((↑(spectrum R a) : Type u_1), R)))
    (𝓤 C((↑(σₙ R a) : Type u_1), R)₀)
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(cfcₙHom_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)

Tactic:
refine (cfcHom_isClosedEmbedding ha).comp <|
    (IsUniformInducing.isUniformEmbedding ⟨?_⟩).isClosedEmbedding

Premises used: cfcHom_isClosedEmbedding, Topology.IsClosedEmbedding.comp, IsUniformInducing.mk, IsUniformEmbedding.isClosedEmbedding, IsUniformInducing.isUniformEmbedding