awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t u : Set X
ht : SeparatedNhds s t
hu : SeparatedNhds s u
⊢ SeparatedNhds s (t ∪ u)

Tactic:
(ht.symm.union_left hu.symm).symm

Premises used: SeparatedNhds.symm, SeparatedNhds.union_left
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsOpen[inst] (s ∪ t)
obtain :
  ∀ (u v : Set X) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hsu : s ⊆ u) (htv : t ⊆ v) (huv : Disjoint u v),
    IsOpen[inst] s
⊢ IsOpen[inst] s

Tactic:
obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
suffices : s = (s ∪ t) ∩ u
⊢ IsOpen[inst] s

Tactic:
suffices s = (s ∪ t) ∩ u from this ▸ hst'.inter hu
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
rw : s = s ∩ u ∪ t ∩ u
rw₁ : s = s ∩ u ∪ ∅
rw₂ : s = s ∩ u
rw₃ rw₄ : s = s
⊢ s = (s ∪ t) ∩ u

Tactic:
rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty,
    inter_eq_left.2 hsu]

Premises used: Set.inter_eq_left, Iff.mpr, Set.union_empty, Disjoint.mono_left, Disjoint.symm, Disjoint.inter_eq, Set.union_inter_distrib_right
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsOpen[inst] (s ∪ t)
⊢ IsOpen[inst] t

Tactic:
hst.symm.isOpen_left_of_isOpen_union (union_comm _ _ ▸ hst')

Premises used: SeparatedNhds.symm, Eq.rec, SeparatedNhds.isOpen_left_of_isOpen_union, Set.union_comm
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
⊢ IsOpen[inst] (s ∪ t) ↔ IsOpen[inst] s ∧ IsOpen[inst] t

Tactic:
⟨fun h ↦ ⟨hst.isOpen_left_of_isOpen_union h, hst.isOpen_right_of_isOpen_union h⟩,
    fun ⟨h1, h2⟩ ↦ h1.union h2⟩

Premises used: SeparatedNhds.isOpen_left_of_isOpen_union, _private.0.SeparatedNhds.isOpen_union_iff.match_1, IsOpen.union, And.intro, Iff.intro, SeparatedNhds.isOpen_right_of_isOpen_union, IsOpen, Union.union
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsClosed[inst] (s ∪ t)
obtain :
  ∀ (u v : Set X) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hsu : s ⊆ u) (htv : t ⊆ v) (huv : Disjoint u v),
    IsClosed[inst] s
⊢ IsClosed[inst] s

Tactic:
obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsClosed[inst] (s ∪ t)
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
rw :
  ∀ (hst' : IsOpen[inst] (s ∪ t)ᶜ) (u v : Set X) (hu : IsOpen[inst] u) (hv : IsOpen[inst] v) (hsu : s ⊆ u) (htv : t ⊆ v)
    (huv : Disjoint u v), IsOpen[inst] sᶜ
⊢ IsClosed[inst] s

Tactic:
rw [← isOpen_compl_iff] at hst' ⊢

Premises used: isOpen_compl_iff
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
suffices : sᶜ = (s ∪ t)ᶜ ∪ v
⊢ IsOpen[inst] sᶜ

Tactic:
suffices sᶜ = (s ∪ t)ᶜ ∪ v from this ▸ hst'.union hv
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
rw : v ⊆ sᶜ
⊢ sᶜ = (s ∪ t)ᶜ ∪ v

Tactic:
rw [← compl_inj_iff, Set.compl_union, compl_compl, compl_compl, union_inter_distrib_right,
    (disjoint_compl_right.mono_left htv).inter_eq, union_empty, left_eq_inter, subset_compl_comm]

Premises used: Set.compl_union, compl_compl, Set.left_eq_inter, Set.union_empty, Set.subset_compl_comm, Disjoint.mono_left, disjoint_compl_right, Disjoint.inter_eq, compl_inj_iff, Set.union_inter_distrib_right
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ v ⊆ sᶜ

Tactic:
(huv.mono_left hsu).subset_compl_left

Premises used: Disjoint.mono_left, Disjoint.subset_compl_left
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst] u
hv : IsOpen[inst] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ v ⊆ sᶜ

Tactic:
exact (huv.mono_left hsu).subset_compl_left

Premises used: Disjoint.mono_left, Disjoint.subset_compl_left
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
hst' : IsClosed[inst] (s ∪ t)
⊢ IsClosed[inst] t

Tactic:
hst.symm.isClosed_left_of_isClosed_union (union_comm _ _ ▸ hst')

Premises used: SeparatedNhds.symm, Eq.rec, Set.union_comm, SeparatedNhds.isClosed_left_of_isClosed_union
-- Module: Mathlib.Topology.Separation.SeparatedNhds
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hst : SeparatedNhds s t
⊢ IsClosed[inst] (s ∪ t) ↔ IsClosed[inst] s ∧ IsClosed[inst] t

Tactic:
⟨fun h ↦ ⟨hst.isClosed_left_of_isClosed_union h, hst.isClosed_right_of_isClosed_union h⟩,
    fun ⟨h1, h2⟩ ↦ h1.union h2⟩

Premises used: SeparatedNhds.isClosed_right_of_isClosed_union, IsClosed.union, IsClosed, And.intro, Iff.intro, Union.union, _private.0.SeparatedNhds.isClosed_union_iff.match_1, SeparatedNhds.isClosed_left_of_isClosed_union
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ seqClosure s

Tactic:
fun p hp =>
  ⟨const ℕ p, fun _ => hp, tendsto_const_nhds⟩

Premises used: Set.Mem, tendsto_const_nhds, setOf, seqClosure, Set.Subset, Nat, And.intro, Exists.intro, Function.const
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ seqClosure s ⊆ closure[inst] s

Tactic:
fun _p ⟨_x, xM, xp⟩ =>
  mem_closure_of_tendsto xp (univ_mem' xM)

Premises used: Membership.mem, Set.Subset, _private.0.seqClosure_subset_closure.match_1, closure, Filter.univ_mem', mem_closure_of_tendsto
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsSeqClosed s
⊢ seqClosure s = s

Tactic:
Subset.antisymm (fun _p ⟨_x, hx, hp⟩ => hs hx hp) subset_seqClosure

Premises used: Set.Subset.antisymm, Membership.mem, _private.0.seqClosure_subset_closure.match_1, subset_seqClosure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : seqClosure s = s
⊢ IsSeqClosed s

Tactic:
fun x _p hxs hxp => hs ▸ ⟨x, hxs, hxp⟩

Premises used: Eq.rec, And.intro, Exists.intro, IsSeqClosed
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsSeqClosed s ↔ seqClosure s = s

Tactic:
⟨IsSeqClosed.seqClosure_eq, isSeqClosed_of_seqClosure_eq⟩

Premises used: IsSeqClosed.seqClosure_eq, Iff.intro, isSeqClosed_of_seqClosure_eq
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hc : IsClosed[inst] s
⊢ IsSeqClosed s

Tactic:
fun _u _x hu hx => hc.mem_of_tendsto hx (Eventually.of_forall hu)

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, IsSeqClosed
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FrechetUrysohnSpace X
s : Set X
⊢ seqClosure s = closure[inst] s

Tactic:
seqClosure_subset_closure.antisymm <| FrechetUrysohnSpace.closure_subset_seqClosure s

Premises used: HasSubset.Subset.antisymm, seqClosure_subset_closure, FrechetUrysohnSpace.closure_subset_seqClosure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FrechetUrysohnSpace X
s : Set X
a : X
rw : a ∈ seqClosure s ↔ ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
⊢ a ∈ closure[inst] s ↔ ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
rw [← seqClosure_eq_closure]

Premises used: seqClosure_eq_closure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : FrechetUrysohnSpace X
s : Set X
a : X
⊢ a ∈ seqClosure s ↔ ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)

Tactic:
rfl
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)

Tactic:
⟨fun hf u hu => hf.comp hu, fun h =>
      ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩

Premises used: Iff.mpr, nhds_basis_closeds, Filter.HasBasis.tendsto_iff, Iff.intro, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
hf :
  ∀ (h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)) (ib : Set Y),
    b ∉ ib ∧ IsClosed[inst_1] ib → ∃ (ia : Set X), (a ∉ ia ∧ IsClosed[inst] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ ibᶜ
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)

Tactic:
refine
    ⟨fun hf u hu => hf.comp hu, fun h =>
      ((nhds_basis_closeds _).tendsto_iff (nhds_basis_closeds _)).2 ?_⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst_1] s
⊢ ∃ (ia : Set X), (a ∉ ia ∧ IsClosed[inst] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ

Tactic:
⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩

Premises used: subset_closure, mt, closure, Set.preimage, And.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst_1] s
refine : a ∈ closure[inst] (f ⁻¹' s) → b ∈ s
⊢ ∃ (ia : Set X), (a ∉ ia ∧ IsClosed[inst] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ

Tactic:
refine ⟨closure (f ⁻¹' s), ⟨mt ?_ hbs, isClosed_closure⟩, fun x => mt fun hx => subset_closure hx⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst_1] s
rw : a ∈ seqClosure (f ⁻¹' s) → b ∈ s
⊢ a ∈ closure[inst] (f ⁻¹' s) → b ∈ s

Tactic:
rw [← seqClosure_eq_closure]

Premises used: seqClosure_eq_closure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst_1] s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s

Tactic:
hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst_1] s
u : ℕ → X
hus : ∀ (n : ℕ), u n ∈ f ⁻¹' s
hu : Tendsto u atTop (𝓝 a)
⊢ b ∈ s

Tactic:
exact hsc.mem_of_tendsto (h u hu) (Eventually.of_forall hus)

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X

Tactic:
⟨fun s x hcx => ?_⟩

Premises used: FrechetUrysohnSpace.mk
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
refine : ∀ (s : Set X) (x : X) (hcx : x ∈ closure[inst] s), x ∈ seqClosure s
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hcx => ?_⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
pos : ∀ (hx : x ∈ s), x ∈ seqClosure s
neg : ∀ (hx : x ∉ s), x ∈ seqClosure s
⊢ x ∈ seqClosure s

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∈ s
⊢ x ∈ seqClosure s

Tactic:
subset_seqClosure hx

Premises used: subset_seqClosure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∈ s
⊢ x ∈ seqClosure s

Tactic:
exact subset_seqClosure hx

Premises used: subset_seqClosure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∉ s
⊢ ∃ (u : ℕ → X), Tendsto u atTop (𝓝 x) ∧ ∃ᶠ (x : ℕ) in atTop, u x ∈ s

Tactic:
simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
        ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,
        not_true_eq_false] using h (· ∉ s) x

Premises used: mem_closure_iff_frequently, Classical.not_not, ContinuousAt, imp_false, Function.comp, Membership.mem, not_true_eq_false, exists_prop, Filter.not_frequently, not_false_eq_true, tendsto_nhds_true, Classical.not_forall, Not
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∉ s
neg : ∀ (u : ℕ → X) (hux : Tendsto u atTop (𝓝 x)) (hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s), x ∈ seqClosure s
⊢ x ∈ seqClosure s

Tactic:
obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by
      simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
        ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,
        not_true_eq_false] using h (· ∉ s) x

Premises used: Filter.atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
neg : ∀ (φ : ℕ → ℕ) (φ_mono : StrictMono φ) (hφ : ∀ (n : ℕ), u (φ n) ∈ s), x ∈ seqClosure s
⊢ x ∈ seqClosure s

Tactic:
rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩

Premises used: Filter.extraction_of_frequently_atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s

Tactic:
⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩

Premises used: Set.Mem, setOf, Function.comp, StrictMono.tendsto_atTop, seqClosure, And.intro, Exists.intro, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
s : Set X
x : X
hcx : x ∈ closure[inst] s
hx : x ∉ s
u : ℕ → X
hux : Tendsto u atTop (𝓝 x)
hus : ∃ᶠ (x : ℕ) in atTop, u x ∈ s
φ : ℕ → ℕ
φ_mono : StrictMono φ
hφ : ∀ (n : ℕ), u (φ n) ∈ s
⊢ x ∈ seqClosure s

Tactic:
exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FirstCountableTopology X
⊢ FrechetUrysohnSpace X

Tactic:
FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto fun _ _ => tendsto_iff_seq_tendsto.2

Premises used: Iff.mpr, Filter.tendsto_iff_seq_tendsto, FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
s : Set X
hs : IsSeqClosed s
rw : closure[inst] s = s
rw₁ : seqClosure s = s
rw₂ rw₃ : s = s
⊢ IsClosed[inst] s

Tactic:
rw [← closure_eq_iff_isClosed, ← seqClosure_eq_closure, hs.seqClosure_eq]

Premises used: closure_eq_iff_isClosed, IsSeqClosed.seqClosure_eq, seqClosure_eq_closure
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
⊢ FrechetUrysohnSpace X

Tactic:
⟨fun s x hx ↦ ?_⟩

Premises used: FrechetUrysohnSpace.mk
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
refine : ∀ (s : Set X) (x : X) (hx : x ∈ closure[inst] s), x ∈ seqClosure s
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : x ∈ closure[inst] s
⊢ ∃ (x_1 : ℕ → Y), (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))

Tactic:
rw [hf.closure_eq_preimage_closure_image, mem_preimage, mem_closure_iff_seq_limit] at hx

Premises used: mem_closure_iff_seq_limit, Topology.IsInducing.closure_eq_preimage_closure_image, Set.mem_preimage
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
hx : ∃ (x_1 : ℕ → Y), (∀ (n : ℕ), x_1 n ∈ f '' s) ∧ Tendsto x_1 atTop (𝓝 (f x))
rcases : ∀ (u : ℕ → Y) (hus : ∀ (n : ℕ), u n ∈ f '' s) (hu : Tendsto u atTop (𝓝 (f x))), x ∈ seqClosure s
⊢ x ∈ seqClosure s

Tactic:
rcases hx with ⟨u, hus, hu⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hus : ∀ (n : ℕ), u n ∈ f '' s
hu : Tendsto u atTop (𝓝 (f x))
choose : ∀ (v : (n : ℕ) → X) (hv : ∀ (n : ℕ), v n ∈ s) (hvu : ∀ (n : ℕ), f (v n) = u n), x ∈ seqClosure s
⊢ x ∈ seqClosure s

Tactic:
choose v hv hvu using hus
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : (n : ℕ) → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ x ∈ seqClosure s

Tactic:
⟨v, hv, ?_⟩

Premises used: Set.Mem, setOf, seqClosure, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : (n : ℕ) → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
refine : Tendsto v atTop (𝓝 x)
⊢ x ∈ seqClosure s

Tactic:
refine ⟨v, hv, ?_⟩
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace Y
f : X → Y
hf : IsInducing f
s : Set X
x : X
u : ℕ → Y
hu : Tendsto u atTop (𝓝 (f x))
v : (n : ℕ) → X
hv : ∀ (n : ℕ), v n ∈ s
hvu : ∀ (n : ℕ), f (v n) = u n
⊢ Tendsto v atTop (𝓝 x)

Tactic:
simpa only [hf.tendsto_nhds_iff, Function.comp_def, hvu]

Premises used: Topology.IsInducing.tendsto_nhds_iff, Function.comp_def
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : FrechetUrysohnSpace X
p : X → Prop
⊢ FrechetUrysohnSpace.{u_1} (Subtype p)

Tactic:
IsInducing.subtypeVal.frechetUrysohnSpace

Premises used: Set.Mem, Topology.IsInducing.frechetUrysohnSpace, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : SequentialSpace X
M : Set X
⊢ IsSeqClosed M ↔ IsClosed[inst] M

Tactic:
⟨IsSeqClosed.isClosed, IsClosed.isSeqClosed⟩

Premises used: IsClosed.isSeqClosed, Iff.intro, IsSeqClosed.isClosed
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
⊢ IsClosed[inst] (⋃ (i : ℕ), closure[inst] {x i})

Tactic:
IsSeqClosed.isClosed fun y l hy hy' => ?_

Premises used: IsSeqClosed.isClosed
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
refine :
  ∀ (y : ℕ → X) (l : X) (hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n))
    (hy' : Tendsto y atTop (𝓝 l)), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
⊢ IsClosed[inst] (⋃ (i : ℕ), closure[inst] {x i})

Tactic:
refine IsSeqClosed.isClosed fun y l hy hy' => ?_

Premises used: IsSeqClosed.isClosed
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
pos :
  ∀ (hm : ∃ (m : ℕ), ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)),
    Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
neg :
  ∀ (hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst] {x m}),
    Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
by_cases! hm : ∃ m, ∃ᶠ n in atTop, y n ∈ closure {x m}

Premises used: Filter.atTop
-- Module: Mathlib.Topology.Sequences
Goal:
X : Type u_1
inst : TopologicalSpace X
x : ℕ → X
inst_1 : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) (y n)
hy' : Tendsto y atTop (𝓝 l)
hm : ∃ (m : ℕ), ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)
pos :
  ∀ (m : ℕ) (pm : ∃ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set X) (closure[inst] {x m}) (y n)),
    Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l
⊢ Membership.mem (γ := Set X) (⋃ (i : ℕ), closure[inst] {x i}) l

Tactic:
obtain ⟨m, pm⟩ := hm