awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
inst_6 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst_4] (⇑φ : (a : C((↑s : Type), ℝ≥0)) → A)
hψ : Continuous[_, inst_4] (⇑ψ : (a : C((↑s : Type), ℝ≥0)) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)),
    let ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
      ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))));
    Continuous[_, inst_4] (⇑ξ' : (a : C((↑s' : Type), ℝ)) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)) → A) (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hφ' :
  Continuous[_, inst_4]
    (⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hψ' :
  Continuous[_, inst_4]
    (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
⊢ Eq (α := A)
    ((ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)

Tactic:
obtain ⟨hψ', hψ_id⟩ := this ψ hψ
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
inst_6 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst_4] (⇑φ : (a : C((↑s : Type), ℝ≥0)) → A)
hψ : Continuous[_, inst_4] (⇑ψ : (a : C((↑s : Type), ℝ≥0)) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)),
    let ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
      ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))));
    Continuous[_, inst_4] (⇑ξ' : (a : C((↑s' : Type), ℝ)) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)) → A) (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hφ' :
  Continuous[_, inst_4]
    (⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hψ' :
  Continuous[_, inst_4]
    (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
⊢ CompactSpace (↑s' : Type)

Tactic:
have hs' : CompactSpace s' := e.compactSpace
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
inst_6 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst_4] (⇑φ : (a : C((↑s : Type), ℝ≥0)) → A)
hψ : Continuous[_, inst_4] (⇑ψ : (a : C((↑s : Type), ℝ≥0)) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)),
    let ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
      ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))));
    Continuous[_, inst_4] (⇑ξ' : (a : C((↑s' : Type), ℝ)) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)) → A) (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hφ' :
  Continuous[_, inst_4]
    (⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hψ' :
  Continuous[_, inst_4]
    (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hs' : CompactSpace (↑s' : Type)
⊢ Eq (α := C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A)
    (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
    (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))

Tactic:
have h' := ContinuousMap.UniqueHom.eq_of_continuous_of_map_id s' _ _ hφ' hψ'
      (hφ_id ▸ hψ_id ▸ h)
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
inst_6 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst_4] (⇑φ : (a : C((↑s : Type), ℝ≥0)) → A)
hψ : Continuous[_, inst_4] (⇑ψ : (a : C((↑s : Type), ℝ≥0)) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this_1 :
  ∀ (ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)),
    let ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
      ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))));
    Continuous[_, inst_4] (⇑ξ' : (a : C((↑s' : Type), ℝ)) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)) → A) (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hφ' :
  Continuous[_, inst_4]
    (⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hψ' :
  Continuous[_, inst_4]
    (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hs' : CompactSpace (↑s' : Type)
h' :
  Eq (α := C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A)
    (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
    (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
this :
  Eq (α := C((↑s : Type), ℝ) →⋆ₐ[ℝ] C((↑s : Type), ℝ))
    (StarAlgHom.comp (B := C((↑s' : Type), ℝ)) (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))
      (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e.symm : C((↑s' : Type), (↑s : Type)))))
    (StarAlgHom.id ℝ C((↑s : Type), ℝ))
h'' : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
⊢ φ = ψ

Tactic:
StarAlgHom.realContinuousMapOfNNReal_injective h''

Premises used: StarAlgHom.realContinuousMapOfNNReal_injective
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
inst_6 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
φ ψ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A
hφ : Continuous[_, inst_4] (⇑φ : (a : C((↑s : Type), ℝ≥0)) → A)
hψ : Continuous[_, inst_4] (⇑ψ : (a : C((↑s : Type), ℝ≥0)) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this_1 :
  ∀ (ξ : C((↑s : Type), ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous[_, inst_4] (⇑ξ : (a : C((↑s : Type), ℝ≥0)) → A)),
    let ξ' : C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A :=
      ξ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))));
    Continuous[_, inst_4] (⇑ξ' : (a : C((↑s' : Type), ℝ)) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)) → A) (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hφ' :
  Continuous[_, inst_4]
    (⇑(φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hψ' :
  Continuous[_, inst_4]
    (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
      (a : C((↑s' : Type), ℝ)) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))) :
          (a : C((↑s' : Type), ℝ)) → A)
        (ContinuousMap.restrict s' (ContinuousMap.id ℝ)) :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)) → A) (ContinuousMap.restrict s (ContinuousMap.id ℝ≥0)) : A)
hs' : CompactSpace (↑s' : Type)
h' :
  Eq (α := C((↑s' : Type), ℝ) →⋆ₐ[ℝ] A)
    (φ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
    (ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type)))))
this :
  Eq (α := C((↑s : Type), ℝ) →⋆ₐ[ℝ] C((↑s : Type), ℝ))
    (StarAlgHom.comp (B := C((↑s' : Type), ℝ)) (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))
      (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e.symm : C((↑s' : Type), (↑s : Type)))))
    (StarAlgHom.id ℝ C((↑s : Type), ℝ))
h'' : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
⊢ φ = ψ

Tactic:
exact StarAlgHom.realContinuousMapOfNNReal_injective h''

Premises used: StarAlgHom.realContinuousMapOfNNReal_injective
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
rw :
  Set.EqOn.{u_1, u_2} (β := A) (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
    (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
    (closure
      (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
        Set (ContinuousMapZero (↑s : Type u_1) 𝕜)))
⊢ φ = ψ

Tactic:
rw [DFunLike.ext'_iff, ← Set.eqOn_univ, ← (ContinuousMapZero.adjoin_id_dense _).closure_eq]

Premises used: DFunLike.ext'_iff, Set.eqOn_univ, Dense.closure_eq, ContinuousMapZero.adjoin_id_dense
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
⊢ Set.EqOn.{u_1, u_2} (β := A) (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
    (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
    (closure
      (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
        Set (ContinuousMapZero (↑s : Type u_1) 𝕜)))

Tactic:
Set.EqOn.closure (fun f hf ↦ ?_) hφ hψ

Premises used: Set.EqOn.closure
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
refine :
  ∀ (f : ContinuousMapZero (↑s : Type u_1) 𝕜)
    (hf :
      f ∈
        (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
              NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
          Set (ContinuousMapZero (↑s : Type u_1) 𝕜))),
    Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) f : A)
      ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) f : A)
⊢ Set.EqOn.{u_1, u_2} (β := A) (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
    (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
    (closure
      (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
            NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
        Set (ContinuousMapZero (↑s : Type u_1) 𝕜)))

Tactic:
refine Set.EqOn.closure (fun f hf ↦ ?_) hφ hψ

Premises used: Set.EqOn.closure
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
f : ContinuousMapZero (↑s : Type u_1) 𝕜
hf :
  f ∈
    (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
      Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
rw :
  Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜))
    (NonUnitalStarAlgHom.equalizer φ ψ) f
⊢ Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) f : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) f : A)

Tactic:
rw [← NonUnitalStarAlgHom.mem_equalizer]

Premises used: NonUnitalStarAlgHom.mem_equalizer
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
f : ContinuousMapZero (↑s : Type u_1) 𝕜
hf :
  f ∈
    (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
      Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
apply : {ContinuousMapZero.id s} ⊆ (↑(NonUnitalStarAlgHom.equalizer φ ψ) : Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜))
    (NonUnitalStarAlgHom.equalizer φ ψ) f

Tactic:
apply adjoin_le ?_ hf

Premises used: NonUnitalStarAlgebra.adjoin_le
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
f : ContinuousMapZero (↑s : Type u_1) 𝕜
hf :
  f ∈
    (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
      Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
rw : ContinuousMapZero.id s ∈ (↑(NonUnitalStarAlgHom.equalizer φ ψ) : Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
⊢ {ContinuousMapZero.id s} ⊆ (↑(NonUnitalStarAlgHom.equalizer φ ψ) : Set (ContinuousMapZero (↑s : Type u_1) 𝕜))

Tactic:
rw [Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : NonUnitalRing A
inst_4 : StarRing A
inst_5 : Module 𝕜 A
inst_6 : IsScalarTower 𝕜 A A
inst_7 : SMulCommClass 𝕜 A A
s : Set 𝕜
hs : CompactSpace.{u_1} (↑s : Type u_1)
h0 : Fact (0 ∈ s)
φ ψ : ContinuousMapZero (↑s : Type u_1) 𝕜 →⋆ₙₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) (ContinuousMapZero.id s) : A)
f : ContinuousMapZero (↑s : Type u_1) 𝕜
hf :
  f ∈
    (↑(adjoin 𝕜 (A := ContinuousMapZero (↑s : Type u_1) 𝕜) {ContinuousMapZero.id s} :
          NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜)) :
      Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
⊢ ContinuousMapZero.id s ∈ (↑(NonUnitalStarAlgHom.equalizer φ ψ) : Set (ContinuousMapZero (↑s : Type u_1) 𝕜))

Tactic:
h

Premises used: Set.Mem, setOf