-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfcₙAux_mem_range_inr (f : C(σₙ 𝕜 a, 𝕜)₀) :
    cfcₙAux hp₁ a ha f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Proof state:
case h.e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
this : Continuous Unitization.fst
⊢ Set.range ⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) = Unitization.fst ⁻¹' {0}

Tactic:
aesop

Result:
no goals

Proof state:
case refine_1.hs
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ ContinuousMapZero.id ⋯ ∈
    ↑(NonUnitalStarSubalgebra.comap (cfcₙAux ⋯ a ha)
        (NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)))

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

Result:
case refine_1.hs
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ ↑a ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ (cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Tactic:
rw [← SetLike.mem_coe]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ (cfcₙAux ⋯ a ha) f ∈ ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))

Proof state:
case refine_2
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
this : Continuous Unitization.fst
⊢ IsClosed (Set.range ⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A))

Tactic:
convert IsClosed.preimage this (isClosed_singleton (x := 0))

Result:
case h.e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
this : Continuous Unitization.fst
⊢ Set.range ⇑(Unitization.inrNonUnitalStarAlgHom 𝕜 A) = Unitization.fst ⁻¹' {0}

Proof state:
case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ ⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}) ⊆
    ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))

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

Result:
case refine_1
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯} ≤
    NonUnitalStarSubalgebra.comap (cfcₙAux ⋯ a ha) (NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))

Proof state:
case refine_1.hs
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : StarModule 𝕜 A
p : A → Prop
p₁ : Unitization 𝕜 A → Prop
hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x
a : A
ha : p a
inst✝¹ : ContinuousFunctionalCalculus 𝕜 p₁
inst✝ : CompleteSpace A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))
⊢ ↑a ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)

Tactic:
exact ⟨a, rfl⟩

Result:
no goals