awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ Continuous[inst_12, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)
have 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
Tactic: rw [← continuousOn_univ] at ha_cont ⊢
Cleared hypotheses: ha_cont, ha, hf, hf0, ha'
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ Continuous[inst_13, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f (a x)
have 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
Tactic: rw [← continuousOn_univ] at ha_cont ⊢
Cleared hypotheses: ha_cont, ha', hf, hf0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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), 𝕜)₀
⊢ σ 𝕜 (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)) → 𝕜)
have simp : σ 𝕜 (A := Unitization 𝕜 A)
    ((cfcHom (p := p₁) sorry : (a : C((↑(σ 𝕜 (↑a : Unitization 𝕜 A)) : Type u_1), 𝕜)) → Unitization 𝕜 A)
        (((Homeomorph.compStarAlgEquiv' 𝕜 𝕜
                (Homeomorph.setCongr (s := σ 𝕜 (A := Unitization 𝕜 A) (↑a : Unitization 𝕜 A)) (t := σₙ 𝕜 a) sorry) :
              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: simp only [NonUnitalStarAlgHom.comp_apply, NonUnitalStarAlgHom.coe_coe]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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), 𝕜)₀
⊢ σ 𝕜 (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)) → 𝕜)
have 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) sorry) :
                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: rw [cfcHom_map_spectrum (hp₁.mpr ha) (R := 𝕜) _]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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)
    (⇑(cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha) : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A)
have 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₁) sorry) : 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) sorry) :
                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: simp only [cfcₙAux, NonUnitalStarAlgHom.coe_comp]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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), 𝕜)))
have 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) sorry) :
            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: refine ((cfcHom_isClosedEmbedding (hp₁.mpr ha)).comp ?_).comp
    ContinuousMapZero.isClosedEmbedding_toContinuousMap
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (hypothesis)
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) (γ := NonUnitalStarSubalgebra 𝕜 (Unitization 𝕜 A))
    (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
    ((cfcₙAux (p := p) (p₁ := p₁) ⋯ a ha : (a : C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀) → Unitization 𝕜 A) f : Unitization 𝕜 A)
have h₁ : Membership.mem (α := Unitization 𝕜 A) (γ := Set (Unitization 𝕜 A))
  (closure[Unitization.instUniformSpace.toTopologicalSpace]
    ((⇑(cfcₙAux (p := p) (p₁ := p₁) sorry 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₁) sorry 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⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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)
have refine_1 : (⇑(cfcₙAux (p := p) (p₁ := p₁) sorry 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: refine closure_minimal ?_ ?_ h₁
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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))
⊢ 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)
have refine_2 : IsClosed[Unitization.instUniformSpace.toTopologicalSpace]
  (↑(NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
    Set (Unitization 𝕜 A))
Tactic: refine closure_minimal ?_ ?_ h₁
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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)
⊢ (⇑(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))
have 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₁) sorry a ha)
      (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A)) :
    NonUnitalStarSubalgebra 𝕜 C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
Tactic: rw [← NonUnitalStarSubalgebra.coe_map, SetLike.coe_subset_coe, NonUnitalStarSubalgebra.map_le]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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)
⊢ 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), 𝕜)₀)
have refine_1 : {ContinuousMapZero.id (σₙ 𝕜 a)} ⊆
  (↑(NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
        (cfcₙAux (p := p) (p₁ := p₁) sorry a ha)
        (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))) :
    Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
Tactic: apply NonUnitalStarAlgebra.adjoin_le
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances (goal)
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)
⊢ {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), 𝕜)₀)
have refine_1 : ContinuousMapZero.id (σₙ 𝕜 a) ∈
  (↑(NonUnitalStarSubalgebra.comap (F := C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀ →⋆ₙₐ[𝕜] Unitization 𝕜 A)
        (cfcₙAux (p := p) (p₁ := p₁) sorry a ha)
        (NonUnitalStarAlgHom.range (F := A →⋆ₙₐ[𝕜] Unitization 𝕜 A) (Unitization.inrNonUnitalStarAlgHom 𝕜 A))) :
    Set C((↑(σₙ 𝕜 a) : Type u_1), 𝕜)₀)
Tactic: apply Set.singleton_subset_iff.mpr