awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
this_1 :
  Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
    (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
        inferInstance ⊓
      UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
this :
  ∀ (U : Set (C(Unit, R) × C(Unit, R))),
    Membership.mem (γ := Filter (C(Unit, R) × C(Unit, R))) (𝓤 C(Unit, R)) U → (0, 0) ∈ U
⊢ Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
    (Filter.comap (β := C(Unit, R) × C(Unit, R))
      (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
        ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
      (𝓤 C(Unit, R)))
    ⊤
have h : ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
  Eq (α := C(Unit, R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
          ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
        (u, v)).1
    0
Tactic: convert! Filter.comap_const_of_mem this with ⟨u, v⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
this_1 :
  Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
    (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
        inferInstance ⊓
      UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
this :
  ∀ (U : Set (C(Unit, R) × C(Unit, R))),
    Membership.mem (γ := Filter (C(Unit, R) × C(Unit, R))) (𝓤 C(Unit, R)) U → (0, 0) ∈ U
h :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := C(Unit, R))
      (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
          (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦
            x.comp 0)
          (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
            ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
          (u, v)).1
      0
⊢ Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
    (Filter.comap (β := C(Unit, R) × C(Unit, R))
      (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
        ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
      (𝓤 C(Unit, R)))
    ⊤
have h₁ : ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
  Eq (α := C(Unit, R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
          ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
        (u, v)).2
    0
Tactic: convert! Filter.comap_const_of_mem this with ⟨u, v⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
this_1 :
  Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
    (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
        inferInstance ⊓
      UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
this :
  ∀ (U : Set (C(Unit, R) × C(Unit, R))),
    Membership.mem (γ := Filter (C(Unit, R) × C(Unit, R))) (𝓤 C(Unit, R)) U → (0, 0) ∈ U
u v : C((↑(σₙ R a) : Type u_1), R)₀
⊢ Eq (α := C(Unit, R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
          ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
        (u, v)).1
    0
have h : Eq (α := R)
  (((Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
            (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦
              x.comp 0)
            (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
              ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
            (u, v)).1 :
        (a : Unit) → R)
      PUnit.unit :
    R)
  ((0 : (a : Unit) → R) PUnit.unit : R)
Tactic: ext ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
this_1 :
  Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
    (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
        inferInstance ⊓
      UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
this :
  ∀ (U : Set (C(Unit, R) × C(Unit, R))),
    Membership.mem (γ := Filter (C(Unit, R) × C(Unit, R))) (𝓤 C(Unit, R)) U → (0, 0) ∈ U
u v : C((↑(σₙ R a) : Type u_1), R)₀
⊢ Eq (α := C(Unit, R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
          ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
        (u, v)).2
    0
have h : Eq (α := R)
  (((Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
            (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦
              x.comp 0)
            (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
              ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
            (u, v)).2 :
        (a : Unit) → R)
      PUnit.unit :
    R)
  ((0 : (a : Unit) → R) PUnit.unit : R)
Tactic: ext ⟨x, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
this_1 :
  Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
    (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
        inferInstance ⊓
      UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
this :
  ∀ (U : Set (C(Unit, R) × C(Unit, R))),
    Membership.mem (γ := Filter (C(Unit, R) × C(Unit, R))) (𝓤 C(Unit, R)) U → (0, 0) ∈ U
⊢ Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
    (Filter.comap (β := C(Unit, R) × C(Unit, R))
      (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
        ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
      (𝓤 C(Unit, R)))
    ⊤
have h : ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
  Eq (α := C(Unit, R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
          ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
        (u, v)).1
    0
Tactic: convert! Filter.comap_const_of_mem this with ⟨u, v⟩ <;>
  ext ⟨x, rfl⟩ <;> [exact map_zero u; exact map_zero v]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : CompleteSpace R
a : A
ha : p a
f : C((↑(spectrum R a) : Type u_1), (↑(σₙ R a) : Type u_1)) :=
  { toFun := Set.inclusion (s := spectrum R a) (t := σₙ R a) ⋯, continuous_toFun := ⋯ }
this_1 :
  Eq.{u_1 + 1} (α := UniformSpace C((↑(σₙ R a) : Type u_1), R)) inferInstance
    (UniformSpace.comap (β := C((↑(spectrum R a) : Type u_1), R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp f)
        inferInstance ⊓
      UniformSpace.comap (β := C(Unit, R)) (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) inferInstance)
this :
  ∀ (U : Set (C(Unit, R) × C(Unit, R))),
    Membership.mem (γ := Filter (C(Unit, R) × C(Unit, R))) (𝓤 C(Unit, R)) U → (0, 0) ∈ U
h :
  ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
    Eq (α := C(Unit, R))
      (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
          (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦
            x.comp 0)
          (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
            ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
          (u, v)).1
      0
⊢ Eq.{u_1 + 1} (α := Filter (C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀))
    (Filter.comap (β := C(Unit, R) × C(Unit, R))
      (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
        ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
      (𝓤 C(Unit, R)))
    ⊤
have h₁ : ∀ (u v : C((↑(σₙ R a) : Type u_1), R)₀),
  Eq (α := C(Unit, R))
    (Function.comp (β := C((↑(σₙ R a) : Type u_1), R) × C((↑(σₙ R a) : Type u_1), R))
        (Prod.map (fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0) fun (x : C((↑(σₙ R a) : Type u_1), R)) ↦ x.comp 0)
        (fun (x : C((↑(σₙ R a) : Type u_1), R)₀ × C((↑(σₙ R a) : Type u_1), R)₀) ↦
          ((↑x.1 : C((↑(σₙ R a) : Type u_1), R)), (↑x.2 : C((↑(σₙ R a) : Type u_1), R))))
        (u, v)).2
    0
Tactic: convert! Filter.comap_const_of_mem this with ⟨u, v⟩ <;>
  ext ⟨x, rfl⟩ <;> [exact map_zero u; exact map_zero v]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (hypothesis)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
⊢ CompactSpace.{u_1} (↑(σₙ R a) : Type u_1)
have h_cpct : CompactSpace.{u_1} (↑(spectrum R a) : Type u_1)
Tactic: have h_cpct : CompactSpace (spectrum R a) := inferInstance
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ContinuousFunctionalCalculus R A p
a : A
h_cpct : CompactSpace.{u_1} (↑(spectrum R a) : Type u_1)
⊢ CompactSpace.{u_1} (↑(σₙ R a) : Type u_1)
have simp : ∀ (h_cpct : IsCompact (spectrum R a)), IsCompact (spectrum R a ∪ {0})
Tactic: simp only [← isCompact_iff_compactSpace, quasispectrum_eq_spectrum_union_zero] at h_cpct ⊢
Cleared hypotheses: h_cpct
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital (goal)
Goal:
R : Type u_1
A : Type u_2
p : A → Prop
inst : Semifield R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : IsTopologicalSemiring R
inst_4 : ContinuousStar R
inst_5 : Ring A
inst_6 : StarRing A
inst_7 : TopologicalSpace A
inst_8 : Algebra R A
inst_9 : ClosedEmbeddingContinuousFunctionalCalculus R A p
inst_10 : ContinuousMapZero.UniqueHom R A
inst_11 : CompleteSpace R
a : A
ha : p a
⊢ IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
    (⇑(cfcₙHom (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
have rw : IsClosedEmbedding.{u_1, u_2} (X := C((↑(σₙ R a) : Type u_1), R)₀) (Y := A)
  (⇑(cfcₙHom_of_cfcHom R (p := p) ha) : (a : C((↑(σₙ R a) : Type u_1), R)₀) → A)
Tactic: rw [cfcₙHom_eq_cfcₙHom_of_cfcHom (R := R) ha]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ f x - g x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) f a - cfc (p := fun (x : A) ↦ 0 ≤ x) g a
have ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: have ha' := SpectrumRestricts.nnreal_of_nonneg ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ f x - g x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) f a - cfc (p := fun (x : A) ↦ 0 ≤ x) g a
have this : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
  (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
Tactic: have : (spectrum ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ))
      (fun x ↦ f x.toNNReal - g x.toNNReal) :=
    fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ cfc (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ f x - g x) a =
    cfc (p := fun (x : A) ↦ 0 ≤ x) f a - cfc (p := fun (x : A) ↦ 0 ≤ x) g a
have rw : cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
  cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a
Tactic: rw [cfc_nnreal_eq_real .., cfc_nnreal_eq_real .., cfc_nnreal_eq_real .., cfc_congr this]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a
have refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)
Tactic: refine cfc_sub _ _ a ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Algebra ℝ A
inst_6 : IsTopologicalRing A
inst_7 : T2Space A
inst_8 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_9 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ spectrum ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (spectrum ℝ≥0 a)
hg : ContinuousOn g (spectrum ℝ≥0 a)
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
this :
  Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
    (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
refine_1 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) (spectrum ℝ a)
⊢ cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) a =
    cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ)) a -
      cfc (p := IsSelfAdjoint) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) a
have refine_2 : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ (↑(g x.toNNReal) : ℝ)) (spectrum ℝ a)
Tactic: refine cfc_sub _ _ a ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ f x - g x) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a - cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a
have ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
Tactic: have ha' := QuasispectrumRestricts.nnreal_of_nonneg ha
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order (hypothesis)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : NonUnitalRing A
inst_2 : PartialOrder A
inst_3 : StarRing A
inst_4 : StarOrderedRing A
inst_5 : Module ℝ A
inst_6 : IsScalarTower ℝ A A
inst_7 : SMulCommClass ℝ A A
inst_8 : IsTopologicalRing A
inst_9 : T2Space A
inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst_11 : NonnegSpectrumClass ℝ A
f g : ℝ≥0 → ℝ≥0
a : A
hfg : ∀ x ∈ σₙ ℝ≥0 a, g x ≤ f x
ha : 0 ≤ a
hf : ContinuousOn f (σₙ ℝ≥0 a)
hf0 : f 0 = 0
hg : ContinuousOn g (σₙ ℝ≥0 a)
hg0 : g 0 = 0
ha' : QuasispectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
⊢ cfcₙ (p := fun (x : A) ↦ 0 ≤ x) (fun (x : ℝ≥0) ↦ f x - g x) a =
    cfcₙ (p := fun (x : A) ↦ 0 ≤ x) f a - cfcₙ (p := fun (x : A) ↦ 0 ≤ x) g a
have this : Set.EqOn (β := ℝ) (fun (x : ℝ) ↦ (↑(f x.toNNReal - g x.toNNReal) : ℝ))
  (fun (x : ℝ) ↦ (↑(f x.toNNReal) : ℝ) - (↑(g x.toNNReal) : ℝ)) (σₙ ℝ a)
Tactic: have : (σₙ ℝ a).EqOn (fun x ↦ ((f x.toNNReal - g x.toNNReal : ℝ≥0) : ℝ))
      (fun x ↦ f x.toNNReal - g x.toNNReal) :=
    fun x hx ↦ NNReal.coe_sub <| hfg _ <| ha'.apply_mem hx