-- Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
Goal:
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : MetricSpace R
inst_3 : Nontrivial R
inst_4 : IsTopologicalSemiring R
inst_5 : ContinuousStar R
inst_6 : NonUnitalRing A
inst_7 : StarRing A
inst_8 : TopologicalSpace A
inst_9 : Module R A
inst_10 : SMulCommClass R A A
inst_11 : IsScalarTower R A A
inst_12 : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
inl :
  ∀ (h_tendsto : TendstoUniformlyOn F f ⊥ (quasispectrum R a))
    (hF : ∀ᶠ (x : X) in ⊥, ContinuousOn (F x) (quasispectrum R a)) (hF0 : ∀ᶠ (x : X) in ⊥, F x 0 = 0),
    Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) ⊥ (𝓝 (cfcₙ (p := p) f a))
inr inr₁ : ∀ (hl : l.NeBot), Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
inr₂ :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (quasispectrum R a)),
    Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
inr₃ :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (quasispectrum R a)) (hf0 : f 0 = 0),
    Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
pos :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (quasispectrum R a)) (hf0 : f 0 = 0) (ha : p a),
    Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
neg neg₁ :
  ∀ (hl : l.NeBot) (hf : ContinuousOn f (quasispectrum R a)) (hf0 : f 0 = 0) (ha : ¬p a),
    Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))

Tactic:
open scoped NonUnitalContinuousFunctionalCalculus in
  obtain (rfl | hl) := l.eq_or_neBot
  · simp
  have hf := h_tendsto.continuousOn hF.frequently
  have hf0 : f 0 = 0 := Eq.symm <|
    tendsto_nhds_unique (tendsto_const_nhds.congr' <| .symm hF0) <|
    h_tendsto.tendsto_at (quasispectrum.zero_mem R a)
  by_cases ha : p a
  · let s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
    have hs : s ∈ l := hF.and hF0
    rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]
    conv =>
      enter [1, x]
      rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]
    rw [cfcₙ_apply ..]
    apply cfcₙHom_continuous _ |>.tendsto _ |>.comp
    rw [ContinuousMapZero.isEmbedding_toContinuousMap.isInducing.tendsto_nhds_iff]
    change Tendsto (fun x : s ↦ (⟨_, x.2.1.restrict⟩ : C(quasispectrum R a, R))) _
      (𝓝 ⟨_, hf.restrict⟩)
    rw [hf.tendsto_restrict_iff_tendstoUniformlyOn (fun x ↦ x.2.1)]
    intro t
    simp only [eventually_comap, Subtype.forall]
    peel h_tendsto t with ht x _
    simp_all
  · simpa [cfcₙ_apply_of_not_predicate a ha] using tendsto_const_nhds

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, tendsto_const_nhds, Subtype.forall, Topology.IsInducing.tendsto_nhds_iff, Topology.IsEmbedding.isInducing, Continuous.tendsto, Filter.eq_or_neBot, cfcₙHom_continuous, NonUnitalContinuousFunctionalCalculus, Function.comp_apply, Filter.eventually_comap, Filter.Tendsto.comp, cfcₙ_apply, rfl