-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma spec_cfcₙAux (f : C(σₙ 𝕜 a, 𝕜)₀) : σ 𝕜 (cfcₙAux hp₁ a ha f) = Set.range f

Proof state:
case h.mpr
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : 𝕜
⊢ x ∈ Set.range ⇑f →
    x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))

Tactic:
rintro ⟨x, rfl⟩

Result:
case h.mpr.intro
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : ↑(σₙ 𝕜 a)
⊢ f x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))

Proof state:
case h
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : 𝕜
⊢ x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f)) ↔
    x ∈ Set.range ⇑f

Tactic:
constructor

Result:
case h.mp
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : 𝕜
⊢ x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f)) →
    x ∈ Set.range ⇑f

case h.mpr
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : 𝕜
⊢ x ∈ Set.range ⇑f →
    x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))

Proof state:
case h.mp
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : 𝕜
⊢ x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f)) →
    x ∈ Set.range ⇑f

case h.mpr
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : 𝕜
⊢ x ∈ Set.range ⇑f →
    x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))

Tactic:
all_goals rintro ⟨x, rfl⟩

Result:
case h.mp.intro
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : ↑(σ 𝕜 ↑a)
⊢ ((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f)) x ∈ Set.range ⇑f

case h.mpr.intro
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : ↑(σₙ 𝕜 a)
⊢ f x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))

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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
⊢ σ 𝕜
      (↑(cfcHom ⋯)
        (((↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))).comp ContinuousMapZero.toContinuousMapHom) f)) =
    Set.range ⇑f

Tactic:
simp only [NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
⊢ σ 𝕜
      ((cfcHom ⋯)
        ((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))) =
    Set.range ⇑f

Proof state:
case h.mpr.intro
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : ↑(σₙ 𝕜 a)
⊢ f x ∈ Set.range ⇑((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f))

Tactic:
exact ⟨⟨x, Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a ▸ x.property⟩, rfl⟩

Result:
no goals

Proof state:
case h.mp.intro
𝕜 : 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₁
f : C(↑(σₙ 𝕜 a), 𝕜)₀
x : ↑(σ 𝕜 ↑a)
⊢ ((Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯)) (ContinuousMapZero.toContinuousMapHom f)) x ∈ Set.range ⇑f

Tactic:
exact ⟨⟨x, (Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a).symm ▸ x.property⟩, rfl⟩

Result:
no goals