awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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)
⊢ φ = ψ
have 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)
Tactic: obtain ⟨hφ', hφ_id⟩ := this φ hφ
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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)
⊢ φ = ψ
have hψ' : Continuous[_, inst_4]
  (⇑(ψ.realContinuousMapOfNNReal.comp (ContinuousMap.compStarAlgHom' ℝ ℝ (↑e : C((↑s : Type), (↑s' : Type))))) :
    (a : C((↑s' : Type), ℝ)) → A)
Tactic: obtain ⟨hψ', hψ_id⟩ := this ψ hψ
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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)
⊢ φ = ψ
have 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)
Tactic: obtain ⟨hψ', hψ_id⟩ := this ψ hψ
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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)
⊢ φ = ψ
have hs' : CompactSpace (↑s' : Type)
Tactic: have hs' : CompactSpace s' := e.compactSpace
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
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)
⊢ φ = ψ
have 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)))))
Tactic: have h' := ContinuousMap.UniqueHom.eq_of_continuous_of_map_id s' _ _ hφ' hψ'
      (hφ_id ▸ hψ_id ▸ h)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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)
⊢ φ = ψ
have 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]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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) 𝕜)))
have 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)
Tactic: refine Set.EqOn.closure (fun f hf ↦ ?_) hφ hψ
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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) 𝕜))
⊢ Eq.{u_2 + 1} (α := A) ((φ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) f : A)
    ((ψ : (a : ContinuousMapZero (↑s : Type u_1) 𝕜) → A) f : A)
have rw : Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜))
  (NonUnitalStarAlgHom.equalizer φ ψ) f
Tactic: rw [← NonUnitalStarAlgHom.mem_equalizer]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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) 𝕜))
⊢ Membership.mem (γ := NonUnitalStarSubalgebra 𝕜 (ContinuousMapZero (↑s : Type u_1) 𝕜))
    (NonUnitalStarAlgHom.equalizer φ ψ) f
have apply : {ContinuousMapZero.id s} ⊆ (↑(NonUnitalStarAlgHom.equalizer φ ψ) : Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
Tactic: apply adjoin_le ?_ hf
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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) 𝕜))
have rw : ContinuousMapZero.id s ∈ (↑(NonUnitalStarAlgHom.equalizer φ ψ) : Set (ContinuousMapZero (↑s : Type u_1) 𝕜))
Tactic: rw [Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
⊢ Continuous.{u_1, u_1} (X := C(X, ℝ)₀) toNNReal
have rw : Continuous (X := C(X, ℝ)₀) (Y := C(X, ℝ≥0)) (_root_.toContinuousMap ∘ toNNReal)
Tactic: rw [continuous_induced_rng]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
⊢ (r • f).toNNReal = r • f.toNNReal
have h : ∀ (x : X), (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
⊢ (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
have pos : ∀ (h : LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)),
  (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
Tactic: by_cases! h : 0 ≤ f x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
r : ℝ≥0
f : C(X, ℝ)₀
x : X
pos :
  ∀ (h : LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)),
    (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
⊢ (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
have neg : ∀ (h : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (0 : ℝ)),
  (↑(((r • f).toNNReal : (a : X) → ℝ≥0) x) : ℝ) = (↑((r • f.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
Tactic: by_cases! h : 0 ≤ f x
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f g : C(X, ℝ)₀
⊢ (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal
have a : Eq (α := C(X, ℝ≥0)) (↑((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) : C(X, ℝ≥0))
  (↑((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) : C(X, ℝ≥0))
Tactic: apply toContinuousMap_injective
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
f g : C(X, ℝ)₀
⊢ (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
have a : Eq (α := C(X, ℝ≥0)) (↑((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) : C(X, ℝ≥0))
  (↑((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) : C(X, ℝ≥0))
Tactic: apply toContinuousMap_injective
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    HSMul.hSMul (α := ℝ) ((MonoidHom.id ℝ : (a : ℝ) → ℝ) r : ℝ)
      (HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A))
have simp : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
  r •
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: simp only [MonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
r : ℝ
f : C(X, ℝ)₀
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
have pos : ∀ (hr : 0 ≤ r),
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (r • f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-(r • f)).toNNReal : A) =
    r •
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
Tactic: by_cases! hr : 0 ≤ r