awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
rw :
  ∀ (ha_cont : ContinuousOn a Set.univ) (hs : ∀ (x : X), IsCompact (s x))
    (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x))
    (hf0 : f 0 = 0) (ha' : ∀ (x : X), 0 ≤ a x),
    ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
x : X
h : Membership.mem (γ := Set X) Set.univ x
⊢ ∀ᶠ (x_1 : X) in 𝓝[Set.univ] x, quasispectrum ℝ≥0 (a x_1) ⊆ s x

Tactic:
simpa using ha x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : X → Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
hs : ∀ (x : X), IsCompact (s x)
ha : ∀ (x₀ : X), ∀ᶠ (x : X) in 𝓝 x₀, quasispectrum ℝ≥0 (a x) ⊆ s x₀
hf : ∀ (x : X), ContinuousOn f (s x)
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ

Tactic:
exact ha_cont.cfcₙ_nnreal f (fun x _ ↦ hs x) (fun x _ ↦ by simpa using ha x) (fun x _ ↦ ha' x)

Premises used: ContinuousOn.cfcₙ_nnreal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
rw :
  ∀ (ha_cont : ContinuousOn a Set.univ) (ha : ∀ (x : X), quasispectrum ℝ≥0 (a x) ⊆ s) (hf : ContinuousOn f s)
    (hf0 : f 0 = 0) (ha' : ∀ (x : X), 0 ≤ a x),
    ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
ha : ∀ (x : X), quasispectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ

Tactic:
ha_cont.cfcₙ_nnreal' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' x)

Premises used: ContinuousOn.cfcₙ_nnreal'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : TopologicalSpace X
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
ha_cont : ContinuousOn a Set.univ
ha : ∀ (x : X), quasispectrum ℝ≥0 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), 0 ≤ a x
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ

Tactic:
exact ha_cont.cfcₙ_nnreal' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' x)

Premises used: ContinuousOn.cfcₙ_nnreal'
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ (x : X), quasispectrum ℝ≥0 (a x))) s
ha_cont : Continuous[inst_13, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
rw :
  ∀ (ha_cont : ContinuousOn a Set.univ) (ha' : ∀ (x : X), 0 ≤ a x) (hf : ContinuousOn f s) (hf0 : f 0 = 0),
    ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ
⊢ Continuous[inst_13, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)

Tactic:
rw [← continuousOn_univ] at ha_cont ⊢

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ (x : X), quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Membership.mem (γ := Filter ℝ≥0)
    (𝓝ˢ (⋃ (x : X), ⋃ (_ : Membership.mem (γ := Set X) Set.univ x), quasispectrum ℝ≥0 (a x))) s

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ (x : X), quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ∀ (x : X), Membership.mem (γ := Set X) Set.univ x → 0 ≤ a x

Tactic:
simpa
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : StarRing A
inst_2 : NormedSpace ℝ A
inst_3 : IsScalarTower ℝ A A
inst_4 : SMulCommClass ℝ A A
inst_5 : ContinuousStar A
inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_7 : PartialOrder A
inst_8 : StarOrderedRing A
inst_9 : NonnegSpectrumClass ℝ A
inst_10 : T2Space A
inst_11 : IsSemitopologicalRing A
inst_12 : CompleteSpace A
inst_13 : TopologicalSpace X
s : Set ℝ≥0
f : ℝ≥0 → ℝ≥0
a : X → A
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝ˢ (⋃ (x : X), quasispectrum ℝ≥0 (a x))) s
ha_cont : ContinuousOn a Set.univ
ha' : ∀ (x : X), 0 ≤ a x
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ ContinuousOn.{u_1, u_2} (Y := A) (fun (x : X) ↦ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)) Set.univ

Tactic:
exact ha_cont.cfcₙ_nnreal_of_mem_nhdsSet f (by simpa) (by simpa)

Premises used: ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet
-- 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₁
⊢ Eq (α := Unitization 𝕜 A)
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)
        (ContinuousMapZero.id (σₙ 𝕜 a)) :
      Unitization 𝕜 A)
    ((↑a : Unitization 𝕜 A) : Unitization 𝕜 A)

Tactic:
cfcHom_id (hp₁.mpr ha)

Premises used: Iff.mpr, spectrum, Set.Mem, cfcHom_id, setOf, quasispectrum, ContinuousMap.comp, IsUnit, resolventSet, Not, ContinuousMap.restrict
-- 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₁
⊢ Continuous[_, Unitization.instUniformSpace.toTopologicalSpace]
    (⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)

Tactic:
(cfcHom_continuous (hp₁.mpr ha)).comp <|
    (ContinuousMap.continuous_precomp _).comp <|
    ContinuousMapZero.isEmbedding_toContinuousMap.continuous

Premises used: Iff.mpr, ContinuousMapZero.isEmbedding_toContinuousMap, cfcHom_continuous, Continuous.comp, ContinuousMap.continuous_precomp, Topology.IsEmbedding.continuous
-- 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₁
⊢ Function.Injective (α := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) (β := Unitization 𝕜 A)
    (⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)

Tactic:
(cfcHom_injective (hp₁.mpr ha)).comp <|
    .comp (Equiv.injective _) ContinuousMapZero.isEmbedding_toContinuousMap.injective

Premises used: Iff.mpr, cfcHom_injective, ContinuousMapZero.isEmbedding_toContinuousMap, Function.Injective.comp, Topology.IsEmbedding.injective, Equiv.injective
-- 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₁
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
simp :
  σ 𝕜 (A := Unitization 𝕜 A)
      ((cfcHom (p := p₁) ⋯ : (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), 𝕜)) :
              (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), 𝕜))
              f)) :
        Unitization 𝕜 A) =
    Set.range (ι := (↑(σₙ 𝕜 a) : Type u_1)) (⇑f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)
⊢ σ 𝕜 (A := Unitization 𝕜 A)
      (((↑(cfcHom (p := p₁) ⋯) : C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜) →⋆ₙₐ[𝕜] Unitization 𝕜 A) :
            (a : C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) → Unitization 𝕜 A)
          ((NonUnitalStarAlgHom.comp
                (↑(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), 𝕜))
                ContinuousMapZero.toContinuousMapHom :
              (a_1 : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜))
            f) :
        Unitization 𝕜 A) =
    Set.range (ι := (↑(σₙ 𝕜 a) : Type u_1)) (⇑f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)

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

Premises used: NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_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₁
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
rw :
  Eq (α := Set 𝕜)
    (Set.range (ι := (↑(σ 𝕜 (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), 𝕜)) :
                (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), 𝕜))
                f) :
            C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
        (a : (↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1)) → 𝕜))
    (Set.range (ι := (↑(σₙ 𝕜 a) : Type u_1)) (⇑f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜))
⊢ σ 𝕜 (A := Unitization 𝕜 A)
      ((cfcHom (p := p₁) ⋯ : (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), 𝕜)) :
              (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), 𝕜))
              f)) :
        Unitization 𝕜 A) =
    Set.range (ι := (↑(σₙ 𝕜 a) : Type u_1)) (⇑f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜)

Tactic:
rw [cfcHom_map_spectrum (hp₁.mpr ha) (R := 𝕜) _]

Premises used: Iff.mpr, cfcHom_map_spectrum
-- 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₁
f : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀
⊢ Eq (α := Set 𝕜)
    (Set.range (ι := (↑(σ 𝕜 (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), 𝕜)) :
                (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), 𝕜))
                f) :
            C((↑(σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) :
        (a : (↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1)) → 𝕜))
    (Set.range (ι := (↑(σₙ 𝕜 a) : Type u_1)) (⇑f : (a : (↑(σₙ 𝕜 a) : Type u_1)) → 𝕜))

Tactic:
simp
-- 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₁
simp :
  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), 𝕜)))
⊢ IsClosedEmbedding (X := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) (Y := Unitization 𝕜 A)
    (⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)

Tactic:
simp only [cfcₙAux, NonUnitalStarAlgHom.coe_comp]

Premises used: cfcₙAux, NonUnitalStarAlgHom.coe_comp
-- 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₁
⊢ 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:
((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp
    ContinuousMapZero.isClosedEmbedding_toContinuousMap

Premises used: Iff.mpr, cfcHom_isClosedEmbedding, Topology.IsClosedEmbedding.comp, ContinuousMapZero.isClosedEmbedding_toContinuousMap