awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
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)
rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.im : ℂ).re) : ℂ)) a
| cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]

Premises used: cfc_im_id, cfc_comp', cfc_real_eq_complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
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)
simp : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
| cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f (↑x.im : ℂ).re) : ℂ)) a

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
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)
rw : cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
| cfc (p := IsSelfAdjoint) f (↑(((ℑ : A →ₗ[ℝ] ↥(selfAdjoint A)) : (a : A) → ↥(selfAdjoint A)) a) : A)

Tactic:
rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]
    simp

Premises used: cfc_im_id, cfc_comp', cfc_real_eq_complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
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)
conv_rhs₁ :
  cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a = cfc (p := IsStarNormal) (fun (x : ℂ) ↦ (↑(f x.im) : ℂ)) a
⊢ 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

Premises used: cfc_im_id, cfc_comp', cfc_real_eq_complex
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : 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) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)
    ((ψ : (a : C((↑s : Type u_1), 𝕜)) → A) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)

Tactic:
h
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : 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)
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)

Tactic:
convert! h using 1
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : 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₁ :
  ∀ (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 : 𝕜)
⊢ 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), 𝕜))

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : 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)
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : 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) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)

Tactic:
exact congr_arg _ (by ext; simp)

Premises used: congr_arg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : 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) (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) : A)

Tactic:
exact congr_arg _ (by ext; simp)

Premises used: congr_arg
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : Ring A
inst_4 : StarRing A
inst_5 : Algebra ℝ A
⊢ ContinuousMap.UniqueHom ℝ A

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : TopologicalSpace A
inst_2 : T2Space A
inst_3 : Ring A
inst_4 : StarRing A
inst_5 : Algebra ℂ A
⊢ ContinuousMap.UniqueHom ℂ A

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Continuous.{u_1, u_1} (X := C(X, ℝ)) toNNReal

Tactic:
continuous_postcomp _

Premises used: ContinuousMap.continuous_postcomp, ContinuousMap.toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
f : C(X, ℝ)
x : X
⊢ (f.toNNReal : (a : X) → ℝ≥0) x = Real.toNNReal ((f : (a : X) → ℝ) x)

Tactic:
rfl

Premises used: NNReal.mk, rfl, Real.toNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : C(X, ℝ)
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) : ℝ)
⊢ (f + g).toNNReal + (-f).toNNReal + (-g).toNNReal = (-(f + g)).toNNReal + f.toNNReal + g.toNNReal

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : C(X, ℝ)
x : X
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 : ℝ)
⊢ (↑(((f + g).toNNReal + (-f).toNNReal + (-g).toNNReal : (a : X) → ℝ≥0) x) : ℝ) =
    (↑(((-(f + g)).toNNReal + f.toNNReal + g.toNNReal : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simp [max_neg_zero, -neg_add_rev]

Premises used: neg_add_rev, max_neg_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ 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:
abel
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : C(X, ℝ)
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) : ℝ)
⊢ (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : C(X, ℝ)
x : X
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 : ℝ)))
⊢ (↑(((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:
simp [max_neg_zero, add_mul, mul_add]

Premises used: add_mul, mul_add, max_neg_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ 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:
abel
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
r : ℝ≥0
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) : ℝ)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
r : ℝ≥0
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
r : ℝ≥0
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) : ℝ)
⊢ Eq.{u_1 + 1} (α := C(X, ℝ≥0)) (toNNReal (-(algebraMap ℝ C(X, ℝ) : (a : ℝ) → C(X, ℝ)) (↑r : ℝ))) 0

Tactic:
ext
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
r : ℝ≥0
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:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq.{u_1 + 1} (α := C(X, ℝ≥0)) (toNNReal 1) 1

Tactic:
toNNReal_algebraMap 1

Premises used: ContinuousMap.toNNReal_algebraMap, ContinuousMap.const, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq.{u_1 + 1} (α := C(X, ℝ≥0)) (toNNReal (-1)) 0

Tactic:
toNNReal_neg_algebraMap 1

Premises used: ContinuousMap.toNNReal_neg_algebraMap, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal 1) : A)
      ((φ : (a : C(X, ℝ≥0)) → A) (ContinuousMap.toNNReal (-1)) : A) =
    1

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
φ : StarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0) A
f g : C(X, ℝ)
⊢ 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))
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
A : Type u_2
inst_1 : Ring A
inst_2 : StarRing A
inst_3 : Algebra ℝ A
inst_4 : TopologicalSpace A
inst_5 : IsSemitopologicalRing A
φ : 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)
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))
⊢ 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)

Tactic:
simp only [map_add, map_mul, sub_mul, mul_sub] at this ⊢

Premises used: mul_sub, map_add, sub_mul, map_mul