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
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
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
h0 : Fact (0 ∈ s)
φ ψ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst_5] (⇑φ : (a : C((↑s : Type), ℝ≥0)₀) → A)
hψ : Continuous[_, inst_5] (⇑ψ : (a : C((↑s : Type), ℝ≥0)₀) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this_1 : Fact (0 ∈ s')
e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
e0' : Eq (α := (↑s : Type)) ((e.symm : (a : (↑s' : Type)) → (↑s : Type)) 0) 0
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) (hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)),
    let ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
      ξ.realContinuousMapZeroOfNNReal.comp
        (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 });
    Continuous[_, inst_5] (⇑ξ' : (a : C((↑s' : Type), ℝ)₀) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hφ' :
  Continuous[_, inst_5]
    (⇑(φ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
⊢ φ = ψ
have hψ' : Continuous[_, inst_5]
  (⇑(ψ.realContinuousMapZeroOfNNReal.comp
        (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
    (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
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
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
h0 : Fact (0 ∈ s)
φ ψ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst_5] (⇑φ : (a : C((↑s : Type), ℝ≥0)₀) → A)
hψ : Continuous[_, inst_5] (⇑ψ : (a : C((↑s : Type), ℝ≥0)₀) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this_1 : Fact (0 ∈ s')
e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
e0' : Eq (α := (↑s : Type)) ((e.symm : (a : (↑s' : Type)) → (↑s : Type)) 0) 0
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) (hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)),
    let ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
      ξ.realContinuousMapZeroOfNNReal.comp
        (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 });
    Continuous[_, inst_5] (⇑ξ' : (a : C((↑s' : Type), ℝ)₀) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hφ' :
  Continuous[_, inst_5]
    (⇑(φ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hψ' :
  Continuous[_, inst_5]
    (⇑(ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
⊢ φ = ψ
have hψ_id : Eq (α := A)
  ((ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
        (a : C((↑s' : Type), ℝ)₀) → A)
      (ContinuousMapZero.id s') :
    A)
  ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : 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
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
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
h0 : Fact (0 ∈ s)
φ ψ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst_5] (⇑φ : (a : C((↑s : Type), ℝ≥0)₀) → A)
hψ : Continuous[_, inst_5] (⇑ψ : (a : C((↑s : Type), ℝ≥0)₀) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this_1 : Fact (0 ∈ s')
e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
e0' : Eq (α := (↑s : Type)) ((e.symm : (a : (↑s' : Type)) → (↑s : Type)) 0) 0
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) (hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)),
    let ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
      ξ.realContinuousMapZeroOfNNReal.comp
        (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 });
    Continuous[_, inst_5] (⇑ξ' : (a : C((↑s' : Type), ℝ)₀) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hφ' :
  Continuous[_, inst_5]
    (⇑(φ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hψ' :
  Continuous[_, inst_5]
    (⇑(ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : 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
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
inst_7 : IsScalarTower ℝ A A
inst_8 : SMulCommClass ℝ A A
inst_9 : T2Space A
s : Set ℝ≥0
hs : CompactSpace (↑s : Type)
h0 : Fact (0 ∈ s)
φ ψ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A
hφ : Continuous[_, inst_5] (⇑φ : (a : C((↑s : Type), ℝ≥0)₀) → A)
hψ : Continuous[_, inst_5] (⇑ψ : (a : C((↑s : Type), ℝ≥0)₀) → A)
h :
  Eq (α := A) ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
s' : Set ℝ := toReal '' s
e : (↑s : Type) ≃ₜ (↑s' : Type) := isEmbedding_coe.homeomorphImage s
this_1 : Fact (0 ∈ s')
e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
e0' : Eq (α := (↑s : Type)) ((e.symm : (a : (↑s' : Type)) → (↑s : Type)) 0) 0
this :
  ∀ (ξ : C((↑s : Type), ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) (hξ : Continuous[_, inst_5] (⇑ξ : (a : C((↑s : Type), ℝ≥0)₀) → A)),
    let ξ' : C((↑s' : Type), ℝ)₀ →⋆ₙₐ[ℝ] A :=
      ξ.realContinuousMapZeroOfNNReal.comp
        (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 });
    Continuous[_, inst_5] (⇑ξ' : (a : C((↑s' : Type), ℝ)₀) → A) ∧
      Eq (α := A) ((ξ' : (a : C((↑s' : Type), ℝ)₀) → A) (ContinuousMapZero.id s') : A)
        ((ξ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hφ' :
  Continuous[_, inst_5]
    (⇑(φ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hφ_id :
  Eq (α := A)
    ((φ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((φ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hψ' :
  Continuous[_, inst_5]
    (⇑(ψ.realContinuousMapZeroOfNNReal.comp
          (nonUnitalStarAlgHom_precomp ℝ { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 })) :
      (a : C((↑s' : Type), ℝ)₀) → A)
hψ_id :
  Eq (α := A)
    ((ψ.realContinuousMapZeroOfNNReal.comp
            (nonUnitalStarAlgHom_precomp ℝ
              { toContinuousMap := (↑e : C((↑s : Type), (↑s' : Type))), map_zero' := e0 }) :
          (a : C((↑s' : Type), ℝ)₀) → A)
        (ContinuousMapZero.id s') :
      A)
    ((ψ : (a : C((↑s : Type), ℝ≥0)₀) → A) (ContinuousMapZero.id s) : A)
hs' : CompactSpace (↑s' : Type)
⊢ φ = ψ
have this₁ : ContinuousMapZero.UniqueHom ℝ A
Tactic: have : ContinuousMapZero.UniqueHom ℝ A := inferInstance
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : StarRing A
inst_10 : TopologicalSpace A
inst_11 : Module R A
inst_12 : IsScalarTower R A A
inst_13 : SMulCommClass R A A
inst_14 : NonUnitalRing B
inst_15 : StarRing B
inst_16 : TopologicalSpace B
inst_17 : Module R B
inst_18 : IsScalarTower R B B
inst_19 : SMulCommClass R B B
inst_20 : Module S A
inst_21 : Module S B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : NonUnitalContinuousFunctionalCalculus R B q
inst_26 : ContinuousMapZero.UniqueHom R B
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst_10, inst_16] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
⊢ (φ : (a : A) → B) (cfcₙ (p := p) f a) = cfcₙ (p := q) f ((φ : (a : A) → B) a)
have this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
Tactic: have : Continuous ψ := hφ
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : StarRing A
inst_10 : TopologicalSpace A
inst_11 : Module R A
inst_12 : IsScalarTower R A A
inst_13 : SMulCommClass R A A
inst_14 : NonUnitalRing B
inst_15 : StarRing B
inst_16 : TopologicalSpace B
inst_17 : Module R B
inst_18 : IsScalarTower R B B
inst_19 : SMulCommClass R B B
inst_20 : Module S A
inst_21 : Module S B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : NonUnitalContinuousFunctionalCalculus R B q
inst_26 : ContinuousMapZero.UniqueHom R B
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst_10, inst_16] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
⊢ (φ : (a : A) → B) (cfcₙ (p := p) f a) = cfcₙ (p := q) f ((φ : (a : A) → B) a)
have h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
Tactic: have h_spec := NonUnitalAlgHom.quasispectrum_apply_subset' (R := R) S φ a
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : StarRing A
inst_10 : TopologicalSpace A
inst_11 : Module R A
inst_12 : IsScalarTower R A A
inst_13 : SMulCommClass R A A
inst_14 : NonUnitalRing B
inst_15 : StarRing B
inst_16 : TopologicalSpace B
inst_17 : Module R B
inst_18 : IsScalarTower R B B
inst_19 : SMulCommClass R B B
inst_20 : Module S A
inst_21 : Module S B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : NonUnitalContinuousFunctionalCalculus R B q
inst_26 : ContinuousMapZero.UniqueHom R B
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst_10, inst_16] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
⊢ (φ : (a : A) → B) (cfcₙ (p := p) f a) = cfcₙ (p := q) f ((φ : (a : A) → B) a)
have hψa : q ((ψ : (a : A) → B) a)
Tactic: have hψa : q (ψ a) := hφa
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (hypothesis)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : StarRing A
inst_10 : TopologicalSpace A
inst_11 : Module R A
inst_12 : IsScalarTower R A A
inst_13 : SMulCommClass R A A
inst_14 : NonUnitalRing B
inst_15 : StarRing B
inst_16 : TopologicalSpace B
inst_17 : Module R B
inst_18 : IsScalarTower R B B
inst_19 : SMulCommClass R B B
inst_20 : Module S A
inst_21 : Module S B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : NonUnitalContinuousFunctionalCalculus R B q
inst_26 : ContinuousMapZero.UniqueHom R B
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst_10, inst_16] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this_1 : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
this :
  Eq (α := C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) (ψ.comp (cfcₙHom (p := p) ha))
    (NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι))
⊢ (φ : (a : A) → B) (cfcₙ (p := p) f a) = cfcₙ (p := q) f ((φ : (a : A) → B) a)
have hf' : ContinuousOn f (quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B))
Tactic: have hf' : ContinuousOn f (quasispectrum R (ψ a)) := hf.mono h_spec
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : StarRing A
inst_10 : TopologicalSpace A
inst_11 : Module R A
inst_12 : IsScalarTower R A A
inst_13 : SMulCommClass R A A
inst_14 : NonUnitalRing B
inst_15 : StarRing B
inst_16 : TopologicalSpace B
inst_17 : Module R B
inst_18 : IsScalarTower R B B
inst_19 : SMulCommClass R B B
inst_20 : Module S A
inst_21 : Module S B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : NonUnitalContinuousFunctionalCalculus R B q
inst_26 : ContinuousMapZero.UniqueHom R B
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst_10, inst_16] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this_1 : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
this :
  Eq (α := C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) (ψ.comp (cfcₙHom (p := p) ha))
    (NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι))
hf' : ContinuousOn f (quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B))
⊢ (φ : (a : A) → B) (cfcₙ (p := p) f a) = cfcₙ (p := q) f ((φ : (a : A) → B) a)
have rw : Eq.{u_5 + 1} (α := B)
  ((φ : (a : A) → B)
      ((cfcₙHom (p := p) ha : (a : C((↑(quasispectrum R a) : Type u_2), R)₀) → A)
          { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry } :
        A) :
    B)
  ((cfcₙHom (p := q) hψa : (a : C((↑(quasispectrum R ((φ : (a : A) → B) a)) : Type u_2), R)₀) → B)
      { toFun := (quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B)).restrict (π := fun (a : R) ↦ R) f,
        continuous_toFun := sorry, map_zero' := sorry } :
    B)
Tactic: rw [cfcₙ_apply .., cfcₙ_apply ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
p : A → Prop
q : B → Prop
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : StarRing R
inst_3 : MetricSpace R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : CommRing S
inst_7 : Algebra R S
inst_8 : NonUnitalRing A
inst_9 : StarRing A
inst_10 : TopologicalSpace A
inst_11 : Module R A
inst_12 : IsScalarTower R A A
inst_13 : SMulCommClass R A A
inst_14 : NonUnitalRing B
inst_15 : StarRing B
inst_16 : TopologicalSpace B
inst_17 : Module R B
inst_18 : IsScalarTower R B B
inst_19 : SMulCommClass R B B
inst_20 : Module S A
inst_21 : Module S B
inst_22 : IsScalarTower R S A
inst_23 : IsScalarTower R S B
inst_24 : NonUnitalContinuousFunctionalCalculus R A p
inst_25 : NonUnitalContinuousFunctionalCalculus R B q
inst_26 : ContinuousMapZero.UniqueHom R B
inst_27 : FunLike F A B
inst_28 : NonUnitalAlgHomClass F S A B
inst_29 : StarHomClass F A B
φ : F
f : R → R
a : A
hf : ContinuousOn f (quasispectrum R a)
hf₀ : f 0 = 0
hφ : Continuous[inst_10, inst_16] (⇑φ : (a : A) → B)
ha : p a
hφa : q ((φ : (a : A) → B) a)
ψ : A →⋆ₙₐ[R] B := NonUnitalStarAlgHom.restrictScalars R (↑φ : A →⋆ₙₐ[S] B)
this : Continuous[inst_10, inst_16] (⇑ψ : (a : A) → B)
h_spec : quasispectrum.{u_2, u_5} R (A := B) ((φ : (a : A) → B) a : B) ⊆ quasispectrum R a
hψa : q ((ψ : (a : A) → B) a)
ι : C((↑(quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) : Type u_2),
  (↑(quasispectrum R a) : Type u_2))₀ :=
  {
    toFun :=
      Set.inclusion (s := quasispectrum.{u_2, u_5} R (A := B) ((ψ : (a : A) → B) a : B)) (t := quasispectrum R a)
        h_spec,
    continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ (φ : (a : A) → B) (cfcₙ (p := p) f a) = cfcₙ (p := q) f ((φ : (a : A) → B) a)
have suffices : Eq (α := C((↑(quasispectrum R a) : Type u_2), R)₀ →⋆ₙₐ[R] B) (ψ.comp (cfcₙHom (p := p) ha))
  (NonUnitalStarAlgHom.comp (cfcₙHom (p := q) hψa) (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι))
Tactic: suffices ψ.comp (cfcₙHom ha) =
      (cfcₙHom hψa).comp (ContinuousMapZero.nonUnitalStarAlgHom_precomp R ι) by
    have hf' : ContinuousOn f (quasispectrum R (ψ a)) := hf.mono h_spec
    rw [cfcₙ_apply .., cfcₙ_apply ..]
    exact DFunLike.congr_fun this _