awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f g : C(X, ℝ)₀
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) =
    0
rw :
  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)) =
    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)
⊢ 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)) =
    0

Tactic:
rw [← this]
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f g : C(X, ℝ)₀
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) =
    0
⊢ 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)) =
    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:
abel
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
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
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
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
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
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))) =
    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:
abel
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ)₀
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) (star f).toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-star f).toNNReal : A) =
    star
      (HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
        ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A))

Tactic:
simp only [star_trivial, star_sub, ← map_star]

Premises used: StarHomClass.map_star, TrivialStar.star_trivial, star_sub
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
hφ : Continuous[_, inst_5] (⇑φ : (a : C(X, ℝ≥0)₀) → A)
dsimp :
  Continuous[_, inst_5] fun (f : C(X, ℝ)₀) ↦
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)
⊢ Continuous[_, inst_5] (⇑φ.realContinuousMapZeroOfNNReal : (a : C(X, ℝ)₀) → A)

Tactic:
dsimp [realContinuousMapZeroOfNNReal]

Premises used: NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : Zero X
A : Type u_2
inst_2 : NonUnitalRing A
inst_3 : StarRing A
inst_4 : Module ℝ A
inst_5 : TopologicalSpace A
inst_6 : IsSemitopologicalRing A
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
hφ : Continuous[_, inst_5] (⇑φ : (a : C(X, ℝ≥0)₀) → A)
⊢ Continuous[_, inst_5] fun (f : C(X, ℝ)₀) ↦
    HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f.toNNReal : A)
      ((φ : (a : C(X, ℝ≥0)₀) → A) (-f).toNNReal : A)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
simp :
  HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f
⊢ Eq.{u_2 + 1} (α := A)
    ((φ.realContinuousMapZeroOfNNReal : (a : C(X, ℝ)₀) → A)
        ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f) :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) f : A)

Tactic:
simp only [realContinuousMapZeroOfNNReal_apply]

Premises used: NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
h :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)₀) → A)
        ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) f : A)
h₁ :
  Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)₀) → A)
        (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A)
convert_to :
  HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f
⊢ HSub.hSub (α := A) (β := A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A)
      ((φ : (a : C(X, ℝ≥0)₀) → A)
          (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
        A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f

Tactic:
convert_to φ f - φ 0 = φ f using 2

Premises used: OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
rw : HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) (0 : A) = (φ : (a : C(X, ℝ≥0)₀) → A) f
rw₁ rw₂ : Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A)
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f

Tactic:
rw [map_zero, sub_zero]

Premises used: sub_zero, map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
⊢ HSub.hSub (α := A) (β := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A) =
    (φ : (a : C(X, ℝ≥0)₀) → A) f

Tactic:
on_goal -1 => rw [map_zero, sub_zero]

Premises used: sub_zero, map_zero
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
h : ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = f
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)₀) → A)
        ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) f : A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
h :
  ∀ (x : X),
    (↑((({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
              (a : X) → ℝ≥0)
            x) :
        ℝ) =
      (↑((f : (a : X) → ℝ≥0) x) : ℝ)
⊢ ({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = f

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
x : X
⊢ (↑((({ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
            (a : X) → ℝ≥0)
          x) :
      ℝ) =
    (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
h : (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = 0
⊢ Eq.{u_2 + 1} (α := A)
    ((φ : (a : C(X, ℝ≥0)₀) → A)
        (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
      A)
    ((φ : (a : C(X, ℝ≥0)₀) → A) 0 : A)

Tactic:
congr
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
h :
  ∀ (x : X),
    (↑(((-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
              (a : X) → ℝ≥0)
            x) :
        ℝ) =
      (↑(((0 : C(X, ℝ≥0)₀) : (a : X) → ℝ≥0) x) : ℝ)
⊢ (-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal = 0

Tactic:
ext x
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
f : C(X, ℝ≥0)₀
x : X
⊢ (↑(((-{ toFun := toReal, continuous_toFun := continuous_coe, map_zero' := ⋯ : C(ℝ≥0, ℝ)₀ }.comp f).toNNReal :
            (a : X) → ℝ≥0)
          x) :
      ℝ) =
    (↑(((0 : C(X, ℝ≥0)₀) : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ ψ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
h₁ : ∀ (f : C(X, ℝ≥0)₀), Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((ψ : (a : C(X, ℝ≥0)₀) → A) f : A)
⊢ φ = ψ

Tactic:
ext f
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
φ ψ : NonUnitalStarAlgHom.{0, u_1, u_2} ℝ≥0 C(X, ℝ≥0)₀ A
h : φ.realContinuousMapZeroOfNNReal = ψ.realContinuousMapZeroOfNNReal
f : C(X, ℝ≥0)₀
⊢ Eq.{u_2 + 1} (α := A) ((φ : (a : C(X, ℝ≥0)₀) → A) f : A) ((ψ : (a : C(X, ℝ≥0)₀) → A) f : A)

Tactic:
simpa using congr($(h) ((ContinuousMapZero.mk ⟨toReal, continuous_coe⟩ rfl).comp f))
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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
⊢ Fact (0 ∈ s')

Tactic:
have : Fact (0 ∈ s') := ⟨0, Fact.out, coe_zero⟩
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : Fact (0 ∈ s')
⊢ Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0

Tactic:
have e0 : e 0 = 0 := rfl
-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
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 : Fact (0 ∈ s')
e0 : Eq (α := (↑s' : Type)) ((e : (a : (↑s : Type)) → (↑s' : Type)) 0) 0
⊢ Eq (α := (↑s : Type)) ((e.symm : (a : (↑s' : Type)) → (↑s : Type)) 0) 0

Tactic:
have e0' : e.symm 0 = 0 := e.symm_apply_eq.mpr e0