-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_congr {f g : R → R} {a : A} (hfg : (σₙ R a).EqOn f g) :
    cfcₙ f a = cfcₙ g a

Proof state:
case pos
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
hfg : Set.EqOn f g (σₙ R a)
h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
⊢ cfcₙ f a = cfcₙ g a

Tactic:
rw [cfcₙ_apply f a (h.2.1.congr hfg) (hfg (quasispectrum.zero_mem R a) ▸ h.2.2) h.1,
  cfcₙ_apply g a h.2.1 h.2.2 h.1]

Result:
case pos
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
hfg : Set.EqOn f g (σₙ R a)
h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
⊢ (cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ⋯) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }

Proof state:
case neg.inl
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
hfg : Set.EqOn f g (σₙ R a)
ha : ¬p a
⊢ cfcₙ f a = cfcₙ g a

Tactic:
simp [cfcₙ_apply_of_not_predicate a ha]

Result:
no goals

Proof state:
case neg.inr.inl.hf
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
hfg : Set.EqOn f g (σₙ R a)
hg : ¬ContinuousOn g (σₙ R a)
⊢ ¬ContinuousOn f (σₙ R a)

Tactic:
exact fun hf ↦ hg (hf.congr hfg.symm)

Result:
no goals

Proof state:
case pos.h.e_6.h.e_toContinuousMap.e_toFun
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
hfg : Set.EqOn f g (σₙ R a)
h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
⊢ (σₙ R a).restrict f = (σₙ R a).restrict g

Tactic:
exact Set.restrict_eq_iff.mpr hfg

Result:
no goals

Proof state:
case neg.inr.inr
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
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ cfcₙ f a = cfcₙ g a

Tactic:
rw [cfcₙ_apply_of_not_map_zero a h0, cfcₙ_apply_of_not_map_zero]

Result:
case neg.inr.inr.hf
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
hfg : Set.EqOn f g (σₙ R a)
h0 : ¬g 0 = 0
⊢ ¬f 0 = 0

Proof state:
case neg.inr.inl
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
hfg : Set.EqOn f g (σₙ R a)
hg : ¬ContinuousOn g (σₙ R a)
⊢ cfcₙ f a = cfcₙ g a

Tactic:
rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn]

Result:
case neg.inr.inl.hf
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
hfg : Set.EqOn f g (σₙ R a)
hg : ¬ContinuousOn g (σₙ R a)
⊢ ¬ContinuousOn f (σₙ R a)

Proof state:
case pos
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
hfg : Set.EqOn f g (σₙ R a)
h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
⊢ (cfcₙHom ⋯) { toFun := (σₙ R a).restrict f, continuous_toFun := ⋯, map_zero' := ⋯ } =
    (cfcₙHom ⋯) { toFun := (σₙ R a).restrict g, continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
congr

Result:
case pos.h.e_6.h.e_toContinuousMap.e_toFun
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
hfg : Set.EqOn f g (σₙ R a)
h : p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0
⊢ (σₙ R a).restrict f = (σₙ R a).restrict g

Proof state:
case neg
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
hfg : Set.EqOn f g (σₙ R a)
h : ¬(p a ∧ ContinuousOn g (σₙ R a) ∧ g 0 = 0)
⊢ cfcₙ f a = cfcₙ g a

Tactic:
simp only [not_and_or] at h

Result:
case neg
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
hfg : Set.EqOn f g (σₙ R a)
h : ¬p a ∨ ¬ContinuousOn g (σₙ R a) ∨ ¬g 0 = 0
⊢ cfcₙ f a = cfcₙ g a