awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto (β := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R)
    (fun (x : { x : X // x ∈ s }) ↦
      { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
        map_zero' := ⋯ })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝 { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ })
have pos : Tendsto (α := { x : X // x ∈ s }) (β := C((↑(quasispectrum R a) : Type u_2), R))
  (Function.comp (β := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) toContinuousMap
    fun (x : { x : X // x ∈ s }) ↦
    { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry,
      map_zero' := sorry })
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (𝓝
    (↑{ toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry, map_zero' := sorry } :
      C((↑(quasispectrum R a) : Type u_2), R)))
Tactic: rw [ContinuousMapZero.isEmbedding_toContinuousMap.isInducing.tendsto_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto (α := { x : X // x ∈ s }) (β := C((↑(quasispectrum R a) : Type u_2), R))
    (Function.comp (β := ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) toContinuousMap
      fun (x : { x : X // x ∈ s }) ↦
      { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
        map_zero' := ⋯ })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
      (↑{ toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ } :
        C((↑(quasispectrum R a) : Type u_2), R)))
have pos : Tendsto
  (fun (x : (↑s : Type u_1)) ↦
    { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := sorry })
  (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (𝓝
    { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := sorry :
      C((↑(quasispectrum R a) : Type u_2), R) })
Tactic: change Tendsto (fun x : s ↦ (⟨_, x.2.1.restrict⟩ : C(quasispectrum R a, R))) _
      (𝓝 ⟨_, hf.restrict⟩)
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto
    (fun (x : (↑s : Type u_1)) ↦
      { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯ })
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
      { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯ :
        C((↑(quasispectrum R a) : Type u_2), R) })
have pos : TendstoUniformlyOn (fun (x : (↑s : Type u_1)) ↦ F (↑x : X)) f (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
  (quasispectrum R a)
Tactic: rw [hf.tendsto_restrict_iff_tendstoUniformlyOn (fun x ↦ x.2.1)]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
t : Set (R × R)
⊢ t ∈ uniformity R →
    ∀ᶠ (n : (↑s : Type u_1)) in comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l,
      ∀ x ∈ quasispectrum R a, (f x, (fun (x : (↑s : Type u_1)) ↦ F (↑x : X)) n x) ∈ t
have pos : t ∈ uniformity R → ∀ᶠ (b : X) in l, ∀ (a_2 : X) (b_1 : a_2 ∈ s), a_2 = b → ∀ x ∈ quasispectrum R a, (f x, F a_2 x) ∈ t
Tactic: simp only [eventually_comap, Subtype.forall]
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x : X | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
t : Set (R × R)
⊢ t ∈ uniformity R → ∀ᶠ (b : X) in l, ∀ (a_2 : X) (b_1 : a_2 ∈ s), a_2 = b → ∀ x ∈ quasispectrum R a, (f x, F a_2 x) ∈ t
have pos : ∀ (ht : t ∈ uniformity R) (x : X) (this : ∀ x_1 ∈ quasispectrum R a, (f x_1, F x x_1) ∈ t) (a_1 : X) (b : a_1 ∈ s),
  a_1 = x → ∀ x ∈ quasispectrum R a, (f x, F a_1 x) ∈ t
Tactic: peel h_tendsto t with ht x _
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have 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))
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
Cleared hypotheses: l, h_tendsto, hF, hF0
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have inr : ∀ (hl : l.NeBot), 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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (goal)
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))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
have 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))
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
-- Lean 4 proof step from Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity (hypothesis)
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
inst_13 : TopologicalSpace X
f : X → R → R
a : A
s : Set X
h_cont :
  ContinuousOn.{u_1, u_2} (Y := R →ᵤ[{quasispectrum R a}] R)
    (fun (x : X) ↦ (ofFun {quasispectrum R a} : (a_1 : R → R) → R →ᵤ[{quasispectrum R a}] R) (f x)) s
hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)
hf0 : ∀ x ∈ s, f x 0 = 0
⊢ ContinuousOn.{u_1, u_3} (Y := A) (fun (x : X) ↦ cfcₙ (p := p) (f x) a) s
have h_cont₁ : ∀ x ∈ s,
  ContinuousWithinAt.{u_1, u_2} (Y := R →ᵤ[{quasispectrum R a}] R)
    (fun (x : X) ↦ (ofFun {quasispectrum R a} : (a_2 : R → R) → R →ᵤ[{quasispectrum R a}] R) (f x)) s x
Tactic: rw [ContinuousOn] at h_cont ⊢
Cleared hypotheses: h_cont, hf, hf0