-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma eqOn_of_cfc_eq_cfc {f g : R → R} {a : A} (h : cfc f a = cfc g a)
    (hf : ContinuousOn f (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
h :
  (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
this :
  { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
x : R
hx : x ∈ spectrum R a
⊢ f x = g x

Tactic:
congrm($(this) ⟨x, hx⟩)

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
h : cfc f a = cfc g a
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ Set.EqOn f g (spectrum R a)

Tactic:
rw [cfc_apply f a, cfc_apply g a] at h

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
h :
  (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
⊢ Set.EqOn f g (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
h :
  (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
⊢ Set.EqOn f g (spectrum R a)

Tactic:
have := (cfcHom_isClosedEmbedding (show p a from ha) (R := R)).injective h

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
h :
  (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
this :
  { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
⊢ Set.EqOn f g (spectrum R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
h :
  (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
this :
  { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
⊢ Set.EqOn f g (spectrum R a)

Tactic:
intro x hx

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f g : R → R
a : A
hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝
hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝
ha : autoParam (p a) _auto✝
h :
  (cfcHom ha) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    (cfcHom ha) { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
this :
  { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } =
    { toFun := (spectrum R a).restrict g, continuous_toFun := ⋯ }
x : R
hx : x ∈ spectrum R a
⊢ f x = g x