-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma eqOn_of_cfcₙ_eq_cfcₙ {f g : R → R} {a : A} (h : cfcₙ f a = cfcₙ g a) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
h : cfcₙ f a = cfcₙ g a
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
⊢ Set.EqOn f g (σₙ 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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
h :
  (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Set.EqOn f g (σₙ R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
h :
  (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
this :
  { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Set.EqOn f g (σₙ R a)

Tactic:
intro x hx

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
h :
  (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
this :
  { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
x : R
hx : x ∈ σₙ R a
⊢ f x = g x

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
h :
  (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Set.EqOn f g (σₙ R a)

Tactic:
have := (cfcₙHom_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✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
h :
  (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
this :
  { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
⊢ Set.EqOn f g (σₙ R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f g : R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
hg : autoParam (ContinuousOn g (σₙ R a)) _auto✝
hg0 : autoParam (g 0 = 0) _auto✝
h :
  (cfcₙHom ha) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ha) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
this :
  { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }
x : R
hx : x ∈ σₙ R a
⊢ f x = g x

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

Result:
no goals