awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (hypothesis)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
Tactic: have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((im · : ℂ → ℂ) '' spectrum ℂ a) := by
    rw [spectrum_imaginaryPart' a] at hf
    refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
    simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
| cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.im : ℂ).re) : ℂ)) a
Tactic: rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
| cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.im : ℂ).re) : ℂ)) a
have simp : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
| cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
Tactic: rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]
    simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have conv_rhs : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
  cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
Tactic: conv_rhs =>
    rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]
    simp
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart (goal)
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℂ A
inst_4 : StarModule ℂ A
inst_5 : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst_6 : ContinuousMap.UniqueHom ℂ A
inst_7 : T2Space A
f : ℝ → ℝ
a : A
hf :
  ContinuousOn f (spectrum.{0, u_1} ℝ (A := A) (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A))
ha : IsStarNormal a
this : ContinuousOn (Y := ℂ) (fun (x : ℂ) ↦ (↑(f x.re) : ℂ)) ((fun (x : ℂ) ↦ (↑x.im : ℂ)) '' spectrum ℂ a)
conv_rhs :
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
⊢ cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a =
    cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)
have conv_rhs₁ : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
Tactic: conv_rhs =>
    rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]
    simp
-- 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 : Ring A
inst_4 : StarRing A
inst_5 : Algebra 𝕜 A
s : Set 𝕜
h_1 : CompactSpace.{u_1} (↑s : Type u_1)
φ ψ : C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : C((↑s : Type u_1), 𝕜)) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
          C((↑s : Type u_1), 𝕜)) :
      A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
          C((↑s : Type u_1), 𝕜)) :
      A)
have h₁ : Eq.{u_2 + 1} (α := A)
  ((φ : (a : C((↑s : Type u_1), 𝕜)) → A)
      ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
        C((↑s : Type u_1), 𝕜)) :
    A)
  ((φ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
Tactic: convert! h using 1
-- 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 : Ring A
inst_4 : StarRing A
inst_5 : Algebra 𝕜 A
s : Set 𝕜
h_1 : CompactSpace.{u_1} (↑s : Type u_1)
φ ψ : C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : C((↑s : Type u_1), 𝕜)) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
h₁ :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
          C((↑s : Type u_1), 𝕜)) :
      A)
    ((φ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
          C((↑s : Type u_1), 𝕜)) :
      A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
        ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
          C((↑s : Type u_1), 𝕜)) :
      A)
have h₂ : Eq.{u_2 + 1} (α := A)
  ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
      ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
        C((↑s : Type u_1), 𝕜)) :
    A)
  ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
Tactic: convert! h using 1
-- 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 : Ring A
inst_4 : StarRing A
inst_5 : Algebra 𝕜 A
s : Set 𝕜
h_1 : CompactSpace.{u_1} (↑s : Type u_1)
φ ψ : C((↑s : Type u_1), 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous[_, inst_1] (⇑φ : (a : C((↑s : Type u_1), 𝕜)) → A)
hψ : Continuous[_, inst_1] (⇑ψ : (a : C((↑s : Type u_1), 𝕜)) → A)
h :
  Eq.{u_2 + 1} (α := A) ((φ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
⊢ Eq (α := C((↑s : Type u_1), 𝕜))
    ((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
      C((↑s : Type u_1), 𝕜))
    (ContinuousMap.restrict s (ContinuousMap.id 𝕜) : C((↑s : Type u_1), 𝕜))
have h₁ : ∀ (a : (↑s : Type u_1)),
  Eq (α := 𝕜)
    ((((Polynomial.toContinuousMapOnAlgHom s : (a : Polynomial 𝕜) → C((↑s : Type u_1), 𝕜)) Polynomial.X :
            C((↑s : Type u_1), 𝕜)) :
          (a : (↑s : Type u_1)) → 𝕜)
        a :
      𝕜)
    ((ContinuousMap.restrict s (ContinuousMap.id 𝕜) : (a : (↑s : Type u_1)) → 𝕜) a : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : C(X, ℝ)
⊢ (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal
have h : ∀ (x : X),
  (↑(((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(((-(f + g)).toNNReal + f.toNNReal + g.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
f g : C(X, ℝ)
x : X
⊢ (↑(((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(((-(f + g)).toNNReal + f.toNNReal + g.toNNReal : (a : X) → ℝ≥0) x) : ℝ)
have h : max (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ)) 0 +
      HAdd.hAdd (α := ℝ) (β := ℝ) (-(f : (a : X) → ℝ) x : ℝ) (max ((f : (a : X) → ℝ) x) 0 : ℝ) +
    HAdd.hAdd (α := ℝ) (β := ℝ) (-(g : (a : X) → ℝ) x : ℝ) (max ((g : (a : X) → ℝ) x) 0 : ℝ) =
  HAdd.hAdd (β := ℝ)
    (HAdd.hAdd (β := ℝ)
      (-HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) +
        max (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ)) 0)
      (max ((f : (a : X) → ℝ) x) 0 : ℝ))
    (max ((g : (a : X) → ℝ) x) 0 : ℝ)
Tactic: simp [max_neg_zero, -neg_add_rev]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace 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 h : ∀ (x : X),
  (↑(((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).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
f g : C(X, ℝ)
x : X
⊢ (↑(((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal : (a : X) → ℝ≥0) x) : ℝ)
have h : max (HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ)) 0 +
      (-HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) (max ((g : (a : X) → ℝ) x) 0 : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) (max ((f : (a : X) → ℝ) x) 0 : ℝ) (max ((g : (a : X) → ℝ) x) 0 : ℝ)) +
    (-HMul.hMul (α := ℝ) (β := ℝ) (max ((f : (a : X) → ℝ) x) 0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) +
      HMul.hMul (α := ℝ) (β := ℝ) (max ((f : (a : X) → ℝ) x) 0 : ℝ) (max ((g : (a : X) → ℝ) x) 0 : ℝ)) =
  -HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) +
        max (HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ)) 0 +
      HMul.hMul (α := ℝ) (β := ℝ) (max ((f : (a : X) → ℝ) x) 0 : ℝ) (max ((g : (a : X) → ℝ) x) 0 : ℝ) +
    (-HMul.hMul (α := ℝ) (β := ℝ) (max ((f : (a : X) → ℝ) x) 0 : ℝ) ((g : (a : X) → ℝ) x : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : X) → ℝ) x : ℝ) +
      (-HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : X) → ℝ) x : ℝ) (max ((g : (a : X) → ℝ) x) 0 : ℝ) +
        HMul.hMul (α := ℝ) (β := ℝ) (max ((f : (a : X) → ℝ) x) 0 : ℝ) (max ((g : (a : X) → ℝ) x) 0 : ℝ)))
Tactic: simp [max_neg_zero, add_mul, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
r : ℝ≥0
⊢ Eq.{u_1 + 1} (α := C(X, ℝ≥0)) (toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ)))
    ((algebraMap ℝ≥0 C(X, ℝ≥0) : (a : ℝ≥0) → C(X, ℝ≥0)) r)
have h : ∀ (a : X),
  (↑(((toNNReal ((algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ)) : C(X, ℝ≥0)) : (a : X) → ℝ≥0) a) : ℝ) =
    (↑((((algebraMap ℝ≥0 C(X, ℝ≥0) : (a : ℝ≥0) → C(X, ℝ≥0)) r : C(X, ℝ≥0)) : (a : X) → ℝ≥0) a) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
r : ℝ≥0
⊢ Eq.{u_1 + 1} (α := C(X, ℝ≥0)) (toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ))) 0
have h : ∀ (a : X),
  (↑(((toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ)) : C(X, ℝ≥0)) : (a : X) → ℝ≥0) a) : ℝ) =
    (↑(((0 : C(X, ℝ≥0)) : (a : X) → ℝ≥0) a) : ℝ)
Tactic: ext
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f g : C(X, ℝ)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A) =
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) *
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)
have this : Eq.{u_2 + 1} (α := A)
  ((φ : (a : C(X, ℝ≥0)) → A) ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) : A)
  ((φ : (a : C(X, ℝ≥0)) → A) ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) : A)
Tactic: have := congr(φ $(f.toNNReal_mul_add_neg_mul_add_mul_neg_eq g))
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f g : C(X, ℝ)
this :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)) → A) ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) : A)
    ((φ : (a : C(X, ℝ≥0)) → A) ((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) : A)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A) =
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) *
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)
have simp : ∀
  (this :
    HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)) +
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) =
      HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)) +
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)),
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A) =
    HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) -
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) -
      (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A))
Tactic: simp only [map_add, map_mul, sub_mul, mul_sub] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique (goal)
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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f g : C(X, ℝ)
this :
  HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)) +
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
      (HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A)
          (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)) +
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)) =
    0
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A) -
      (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) -
          HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) -
        (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
          HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
            ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A))) =
    0
have h : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A) -
    (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) -
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A) -
      (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
        HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A))) =
  HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)) → A) (f * g).toNNReal : A)
        (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)) +
      HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) -
    (HAdd.hAdd (α := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f * g)).toNNReal : A)
        (HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
          ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)) +
      HMul.hMul (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A))
Tactic: convert! this using 1
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f g : C(X, ℝ)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A) =
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) +
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)
have this : Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)) → A) ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) : A)
  ((φ : (a : C(X, ℝ≥0)) → A) ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) : A)
Tactic: have := congr(φ $(f.toNNReal_add_add_neg_add_neg_eq g))
-- 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
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f g : C(X, ℝ)
this :
  Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)) → A) ((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal) : A)
    ((φ : (a : C(X, ℝ≥0)) → A) ((-(f + g)).toNNReal + f.toNNReal + g.toNNReal) : A)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A) =
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A) +
      HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A)
have this₁ : HAdd.hAdd (β := A)
    (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (f + g).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (-f).toNNReal : A))
    ((φ : (a : C(X, ℝ≥0)) → A) (-g).toNNReal : A) =
  HAdd.hAdd (β := A)
    (HAdd.hAdd (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (-(f + g)).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)) → A) f.toNNReal : A))
    ((φ : (a : C(X, ℝ≥0)) → A) g.toNNReal : A)
Tactic: simp only [map_add] at this ⊢
Cleared hypotheses: this