awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
refine :
  IsClosedEmbedding (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (Y :=
    C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))
    (⇑(↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜
                (Homeomorph.setCongr (s := σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) (t := σₙ 𝕜 a) ⋯) :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) ≃⋆ₐ[𝕜]
                C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
          C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
      (a_1 : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) → C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))
⊢ IsClosedEmbedding (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) (Y := Unitization 𝕜 A)
    (Function.comp (β := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜))
      (Function.comp (β := C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))
        (⇑(↑(cfcHom (p := p₁) ⋯) : C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] Unitization 𝕜 A) :
          (a : C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) → Unitization 𝕜 A)
        (⇑(↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜
                    (Homeomorph.setCongr (s := σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) (t := σₙ 𝕜 a) ⋯) :
                  C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) ≃⋆ₐ[𝕜]
                    C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
          (a_1 : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) → C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)))
      (⇑ContinuousMapZero.toContinuousMapHom : (a_1 : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)))

Tactic:
refine ((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp
    ContinuousMapZero.isClosedEmbedding_toContinuousMap

Premises used: Iff.mpr, cfcHom_isClosedEmbedding, Topology.IsClosedEmbedding.comp, ContinuousMapZero.isClosedEmbedding_toContinuousMap
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
e : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) ≃ₜ C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜) :=
  Homeomorph.arrowCongr (Homeomorph.setCongr (s := σₙ 𝕜 a) (t := σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) ⋯)
    (Homeomorph.refl 𝕜)
⊢ IsClosedEmbedding (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (Y :=
    C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))
    (⇑(↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜
                (Homeomorph.setCongr (s := σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) (t := σₙ 𝕜 a) ⋯) :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) ≃⋆ₐ[𝕜]
                C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
          C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
      (a_1 : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) → C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))

Tactic:
e.isClosedEmbedding

Premises used: Set.Mem, ContinuousMap.comp, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
e : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) ≃ₜ C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜) :=
  Homeomorph.arrowCongr (Homeomorph.setCongr (s := σₙ 𝕜 a) (t := σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) ⋯)
    (Homeomorph.refl 𝕜)
⊢ IsClosedEmbedding (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) (Y :=
    C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))
    (⇑(↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜
                (Homeomorph.setCongr (s := σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) (t := σₙ 𝕜 a) ⋯) :
              C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) ≃⋆ₐ[𝕜]
                C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
          C((↑(σₙ 𝕜 a) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
      (a_1 : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)) → C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))

Tactic:
exact e.isClosedEmbedding

Premises used: Homeomorph.isClosedEmbedding
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
⊢ Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)

Tactic:
have h₁ := (continuous_cfcₙAux hp₁ a ha).range_subset_closure_image_dense
    (ContinuousMapZero.adjoin_id_dense (σₙ 𝕜 a)) ⟨f, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
⊢ Membership.mem (α := Unitization 𝕜 A)
    (↑(NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
      Set (Unitization 𝕜 A))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)

Tactic:
closure_minimal ?_ ?_ h₁

Premises used: closure_minimal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
refine_1 :
  (⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
      (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
            NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
        Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) ⊆
    (↑(NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
      Set (Unitization 𝕜 A))
refine_2 :
  IsClosed[Unitization.instUniformSpace.toTopologicalSpace]
    (↑(NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
      Set (Unitization 𝕜 A))
⊢ Membership.mem (α := Unitization 𝕜 A)
    (↑(NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
      Set (Unitization 𝕜 A))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)

Tactic:
refine closure_minimal ?_ ?_ h₁

Premises used: closure_minimal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
refine_1 :
  LE.le (α := NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
    (NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
      NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
    (NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
        (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
        (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
      NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
⊢ (⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
      (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
            NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
        Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) ⊆
    (↑(NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
      Set (Unitization 𝕜 A))

Tactic:
rw [← NonUnitalStarSubalgebra.coe_map, SetLike.coe_subset_coe, NonUnitalStarSubalgebra.map_le]

Premises used: SetLike.coe_subset_coe, NonUnitalStarSubalgebra.coe_map, NonUnitalStarSubalgebra.map_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
refine_1 :
  {ContinuousMapZero.id (σₙ 𝕜 a)} ⊆
    (↑(NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
          (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
          (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))) :
      Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
⊢ LE.le (α := NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
    (NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
      NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
    (NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
        (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
        (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
      NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)

Tactic:
apply NonUnitalStarAlgebra.adjoin_le

Premises used: NonUnitalStarAlgebra.adjoin_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
refine_1 :
  ContinuousMapZero.id (σₙ 𝕜 a) ∈
    (↑(NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
          (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
          (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))) :
      Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
⊢ {ContinuousMapZero.id (σₙ 𝕜 a)} ⊆
    (↑(NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
          (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
          (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))) :
      Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)

Tactic:
apply Set.singleton_subset_iff.mpr

Premises used: Iff.mpr, Set.singleton_subset_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
refine_1 :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (Unitization 𝕜 A))
    (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
    (↑a : Unitization 𝕜 A)
⊢ ContinuousMapZero.id (σₙ 𝕜 a) ∈
    (↑(NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
          (cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha)
          (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))) :
      Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)

Tactic:
rw [SetLike.mem_coe, NonUnitalStarSubalgebra.mem_comap, cfcₙAux_id hp₁ a ha]

Premises used: NonUnitalStarSubalgebra.mem_comap, cfcₙAux_id, SetLike.mem_coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (Unitization 𝕜 A))
    (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
    (↑a : Unitization 𝕜 A)

Tactic:
⟨a, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (Unitization 𝕜 A))
    (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
    (↑a : Unitization 𝕜 A)

Tactic:
exact ⟨a, rfl⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
⊢ IsClosed[Unitization.instUniformSpace.toTopologicalSpace]
    (Set.preimage (β := 𝕜) (fun (x : Unitization 𝕜 A) ↦ x.toProd.1) {0})

Tactic:
IsClosed.preimage (Unitization.continuous_fst (𝕜 := 𝕜)) isClosed_singleton

Premises used: IsClosed.preimage, isClosed_singleton, Unitization.continuous_fst
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NonUnitalNormedRing A
inst_2 : StarRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : IsScalarTower 𝕜 A A
inst_5 : SMulCommClass 𝕜 A A
inst_6 : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ (↑x : Unitization 𝕜 A) ↔ p x
a : A
ha : p a
inst_7 : ClosedEmbeddingContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁
inst_8 : CompleteSpace A
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
h₁ :
  Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
    (closure[Unitization.instUniformSpace.toTopologicalSpace]
      ((⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) ''
        (↑(NonUnitalStarAlgebra.adjoin 𝕜 (A := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) {ContinuousMapZero.id (σₙ 𝕜 a)} :
              NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) :
          Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
h :
  Eq (α := Set (Unitization 𝕜 A))
    (Set.range (ι := A) (⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) : (a : A) → Unitization 𝕜 A))
    (Set.preimage (β := 𝕜) (fun (x : Unitization 𝕜 A) ↦ x.toProd.1) {0})
refine_2 : 𝕜
⊢ IsClosed[Unitization.instUniformSpace.toTopologicalSpace]
    (Set.range (ι := A) (⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) : (a : A) → Unitization 𝕜 A))

Tactic:
convert! IsClosed.preimage (Unitization.continuous_fst (𝕜 := 𝕜)) isClosed_singleton

Premises used: IsClosed.preimage, isClosed_singleton, Unitization.continuous_fst