awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
⊢ f 0 = 0

Tactic:
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)
-- 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
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
pos : ∀ (ha : p a), Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))
neg : ∀ (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:
by_cases ha : p a
-- 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
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}
⊢ s ∈ l

Tactic:
have hs : s ∈ l := hF.and hF0
-- 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
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
⊢ Set.range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ∈ l

Tactic:
simpa
-- 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
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
pos :
  Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))
⊢ Tendsto (fun (x : X) ↦ cfcₙ (p := p) (F x) a) l (𝓝 (cfcₙ (p := p) f a))

Tactic:
rw [← tendsto_comap'_iff (i := ((↑) : s → X)) (by simpa)]

Premises used: Filter.tendsto_comap'_iff
-- 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
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
h : ∀ (x : { x : X // x ∈ s }), (((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) x : A)
| Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))

Tactic:
enter [1, x]
-- 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
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
x : { x : X // x ∈ s }
h :
  ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
      { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
        map_zero' := ⋯ } :
    A)
| (((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) x : A)

Tactic:
rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]

Premises used: And.right, And.left, Function.comp_apply, cfcₙ_apply, Subtype.property
-- 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
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
h :
  ∀ (x : { x : X // x ∈ s }),
    ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
        { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
          map_zero' := ⋯ } :
      A)
| Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))

Tactic:
enter [1, x]
      rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]

Premises used: Function.comp_apply
-- 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
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
pos :
  Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      (cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
        { 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) (𝓝 (cfcₙ (p := p) f a))
⊢ Tendsto (α := { x : X // x ∈ s }) ((fun (x : X) ↦ cfcₙ (p := p) (F x) a) ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l) (𝓝 (cfcₙ (p := p) f a))

Tactic:
conv =>
      enter [1, x]
      rw [Function.comp_apply, cfcₙ_apply (hf := x.2.1) (hf0 := x.2.2)]

Premises used: Function.comp_apply
-- 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
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
pos :
  Tendsto.{u_1, u_3} (β := A)
    (fun (x : { x : X // x ∈ s }) ↦
      ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
          { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
            map_zero' := ⋯ } :
        A))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
        ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
          { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }) :
      Filter A)
⊢ Tendsto
    (fun (x : { x : X // x ∈ s }) ↦
      (cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
        { 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) (𝓝 (cfcₙ (p := p) f a))

Tactic:
rw [cfcₙ_apply ..]

Premises used: cfcₙ_apply
-- 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
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
pos :
  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' := ⋯ })
⊢ Tendsto.{u_1, u_3} (β := A)
    (fun (x : { x : X // x ∈ s }) ↦
      ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
          { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) (F (↑x : X)), continuous_toFun := ⋯,
            map_zero' := ⋯ } :
        A))
    (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) l)
    (𝓝
        ((cfcₙHom (p := p) ha : (a : ContinuousMapZero (↑(quasispectrum R a) : Type u_2) R) → A)
          { toFun := (quasispectrum R a).restrict (π := fun (a : R) ↦ R) f, continuous_toFun := ⋯, map_zero' := ⋯ }) :
      Filter A)

Tactic:
apply cfcₙHom_continuous _ |>.tendsto _ |>.comp

Premises used: Continuous.tendsto, cfcₙHom_continuous, Filter.Tendsto.comp
-- 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
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
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 := ⋯,
        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)))
⊢ 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' := ⋯ })

Tactic:
rw [ContinuousMapZero.isEmbedding_toContinuousMap.isInducing.tendsto_nhds_iff]

Premises used: ContinuousMapZero.isEmbedding_toContinuousMap, Topology.IsInducing.tendsto_nhds_iff, Topology.IsEmbedding.isInducing
-- 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
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
pos :
  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) })
⊢ 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)))

Tactic:
change Tendsto (fun x : s ↦ (⟨_, x.2.1.restrict⟩ : C(quasispectrum R a, R))) _
      (𝓝 ⟨_, hf.restrict⟩)

Premises used: ContinuousMap.mk, quasispectrum, nhds, And.left, Filter.Tendsto, ContinuousOn.restrict, Set.restrict, Subtype.val, Subtype.property
-- 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
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
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)
⊢ 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) })

Tactic:
rw [hf.tendsto_restrict_iff_tendstoUniformlyOn (fun x ↦ x.2.1)]
-- 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
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)
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
⊢ 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

Tactic:
simp only [eventually_comap, Subtype.forall]

Premises used: Subtype.forall, Filter.eventually_comap
-- 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
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)
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
⊢ 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:
peel h_tendsto t with ht x _
-- 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
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)
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:
simp_all