awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
⊢ MapClusterPt x F u ↔ ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in F, u a ∈ s

Tactic:
(𝓝 x).basis_sets.mapClusterPt_iff_frequently

Premises used: Set.Mem, nhds, Filter.basis_sets, Filter.HasBasis.mapClusterPt_iff_frequently
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
h : MapClusterPt x F u
p : X → Prop
hp : ∀ᶠ (y : X) in 𝓝 x, p y
⊢ ∃ᶠ (a : α) in F, p (u a)

Tactic:
h.clusterPt.frequently hp

Premises used: MapClusterPt.clusterPt, Set.Mem, Filter.Eventually, setOf, Filter.Frequently, Set.preimage, ClusterPt.frequently, Not
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
β : Type u_2
F : Filter α
x : X
φ : α → β
u : β → X
⊢ MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (map φ F) u

Tactic:
Iff.rfl

Premises used: Set.Mem, Filter.map, Iff.rfl, setOf, Set.preimage, MapClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
inst_1 : F.NeBot
h : Tendsto u F (𝓝 x)
⊢ MapClusterPt x F u

Tactic:
.of_le_nhds h

Premises used: ClusterPt.of_le_nhds, MapClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
β : Type u_2
F : Filter α
u : α → X
x : X
φ : β → α
p : Filter β
h : Tendsto φ p F
H : MapClusterPt x p (u ∘ φ)
⊢ MapClusterPt x F u

Tactic:
H.clusterPt.mono <| map_mono h

Premises used: Filter.map_mono, ClusterPt.mono, MapClusterPt.clusterPt, MapClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
l : X
s : Set X
f : α → X
b : Filter α
hs : IsClosed[inst] s
hf : MapClusterPt l b f
h : ∀ᶠ (x : α) in b, f x ∈ s
⊢ l ∈ s

Tactic:
(hf.frequently' h).mem_of_closed hs

Premises used: ClusterPt.frequently', Filter.Frequently.mem_of_closed
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_3
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
inst_3 : Nonempty ι
x : ι → X
a : X
⊢ MapClusterPt a atTop x ↔ ∀ (i : ι), a ∈ closure[inst] (x '' Ici i)

Tactic:
simp [MapClusterPt, (atTop_basis.map x).clusterPt_iff_forall_mem_closure]

Premises used: Filter.atTop_basis, Filter.HasBasis.map, MapClusterPt, Filter.HasBasis.clusterPt_iff_forall_mem_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F G : Filter X
⊢ AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G

Tactic:
simp only [AccPt, inf_sup_left, sup_neBot]

Premises used: inf_sup_left, Filter.sup_neBot, AccPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : (𝓝[≠] x ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
rw₁ : (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
rw₂ : (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot
rw₃ rw₄ : (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot ↔ (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)

Tactic:
rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]

Premises used: nhdsWithin, ClusterPt, AccPt, inf_assoc
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ 𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
rw₁ : ClusterPt x (𝓟 ({x}ᶜ ∩ C)) ↔ ClusterPt x (𝓟 (C \ {x}))
rw₂ : ClusterPt x (𝓟 (C ∩ {x}ᶜ)) ↔ ClusterPt x (𝓟 (C \ {x}))
rw₃ rw₄ : ClusterPt x (𝓟 (C ∩ {x}ᶜ)) ↔ ClusterPt x (𝓟 (C ∩ {x}ᶜ))
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))

Tactic:
rw [accPt_iff_clusterPt, inf_principal, inter_comm, diff_eq]

Premises used: Filter.inf_principal, Set.diff_eq, Set.inter_comm, accPt_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ∀ U ∈ 𝓝 x, ∃ y ∈ U ∩ C, y ≠ x

Tactic:
simp [accPt_principal_iff_clusterPt, clusterPt_principal_iff, Set.Nonempty,
    and_assoc]

Premises used: clusterPt_principal_iff, Set.Nonempty, and_assoc, accPt_principal_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C

Tactic:
simp [accPt_principal_iff_clusterPt, clusterPt_principal_iff_frequently, and_comm]

Premises used: and_comm, accPt_principal_iff_clusterPt, clusterPt_principal_iff_frequently
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
⊢ (∃ᶠ (x_1 : X) in 𝓝 x, Membership.mem (γ := Set X) {x}ᶜ x_1 ∧ x_1 ∈ C) ↔
    ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z

Tactic:
simp only [and_comm]

Premises used: and_comm
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
⊢ (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z

Tactic:
have : (∃ᶠ z in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ z in 𝓝 x, z ∈ C ∧ z ∈ ({x} : Set X)ᶜ :=
    frequently_inf_principal.trans <| by simp only [and_comm]
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
rw : (∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C

Tactic:
rw [accPt_iff_frequently, this]

Premises used: accPt_iff_frequently
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
a : ∀ (x_1 : X), x_1 ≠ x ∧ x_1 ∈ C ↔ x_1 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_1
⊢ (∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z

Tactic:
congr! 2
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : ClusterPt x (𝓟 (s \ {x})) ↔ (𝓝[s \ {x}] x).NeBot
rw₁ : (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝[s \ {x}] x).NeBot
rw₂ rw₃ : (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot
⊢ AccPt x (𝓟 s) ↔ (𝓝[s \ {x}] x).NeBot

Tactic:
rw [accPt_principal_iff_clusterPt, ClusterPt, nhdsWithin]

Premises used: nhdsWithin, ClusterPt, accPt_principal_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F G : Filter X
h : AccPt x F
hFG : F ≤ G
⊢ AccPt x G

Tactic:
NeBot.mono h (inf_le_inf_left _ hFG)

Premises used: Filter.NeBot.mono, inf_le_inf_left, AccPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
h : AccPt x F
⊢ ClusterPt x F

Tactic:
(accPt_iff_clusterPt.mp h).mono inf_le_right

Premises used: ClusterPt.mono, inf_le_right, Iff.mp, accPt_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
mp : ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)
mpr : x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
constructor
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
mp : ∀ (hc : x ∉ C ∧ ¬AccPt x (𝓟 C)), False
⊢ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
by_contra! hc
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬AccPt x (𝓟 C)
⊢ x ∉ C ∧ ¬ClusterPt x (𝓟 (C \ {x}))

Tactic:
rw [accPt_principal_iff_clusterPt] at hc

Premises used: accPt_principal_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬ClusterPt x (𝓟 (C \ {x}))
⊢ False

Tactic:
simp_all only [not_false_eq_true, diff_singleton_eq_self, not_true_eq_false, hc.1]

Premises used: Set.diff_singleton_eq_self, not_true_eq_false, And.left, not_false_eq_true
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : x ∈ C
⊢ ClusterPt x (𝓟 C)

Tactic:
clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩

Premises used: Iff.mpr, clusterPt_principal_iff, mem_of_mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : x ∈ C
⊢ ClusterPt x (𝓟 C)

Tactic:
exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩

Premises used: Iff.mpr, clusterPt_principal_iff, mem_of_mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C)

Tactic:
h.clusterPt

Premises used: AccPt.clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C)

Tactic:
exact h.clusterPt

Premises used: AccPt.clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
simp : IsClosed[inst] (⋂ i ∈ f, {x : X | x ∈ closure[inst] i})
⊢ IsClosed[inst] {x : X | ClusterPt x f}

Tactic:
simp only [clusterPt_iff_forall_mem_closure, setOf_forall]

Premises used: clusterPt_iff_forall_mem_closure, Set.setOf_forall
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
⊢ IsClosed[inst] (⋂ i ∈ f, {x : X | x ∈ closure[inst] i})

Tactic:
isClosed_biInter fun _ _ ↦ isClosed_closure

Premises used: isClosed_biInter, isClosed_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
⊢ IsClosed[inst] (⋂ i ∈ f, {x : X | x ∈ closure[inst] i})

Tactic:
exact isClosed_biInter fun _ _ ↦ isClosed_closure

Premises used: isClosed_biInter, isClosed_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst] s ↔ ClusterPt x (𝓟 s)

Tactic:
mem_closure_iff_frequently.trans clusterPt_principal_iff_frequently.symm

Premises used: mem_closure_iff_frequently, Iff.trans, clusterPt_principal_iff_frequently, Iff.symm
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst] s ↔ 𝓝 x ⊓ 𝓟 s ≠ ⊥

Tactic:
mem_closure_iff_clusterPt.trans neBot_iff

Premises used: Filter.neBot_iff, mem_closure_iff_clusterPt, Iff.trans
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst] s ↔ (𝓝[s] x).NeBot

Tactic:
mem_closure_iff_clusterPt

Premises used: nhdsWithin, mem_closure_iff_clusterPt, ClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : ¬(𝓝[s] x).NeBot ↔ 𝓝[s] x = ⊥
rw₁ rw₂ : 𝓝[s] x = ⊥ ↔ 𝓝[s] x = ⊥
⊢ x ∉ closure[inst] s ↔ 𝓝[s] x = ⊥

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]

Premises used: mem_closure_iff_nhdsWithin_neBot, Filter.not_neBot
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : x ∈ interior s ↔ x ∉ closure[inst] sᶜ
rw₁ : x ∈ interior s ↔ x ∉ (interior s)ᶜ
rw₂ : x ∈ interior s ↔ ¬x ∉ interior s
rw₃ rw₄ : x ∈ interior s ↔ x ∈ interior s
⊢ x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ)

Tactic:
rw [← mem_closure_iff_clusterPt, closure_compl, mem_compl_iff, not_not]

Premises used: Classical.not_not, mem_closure_iff_clusterPt, closure_compl, Set.mem_compl_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
y : X
inl : ∀ [(𝓝[≠] y).NeBot], Membership.mem (γ := Set X) (closure[inst] {y}ᶜ) y
inr : ∀ (hne : y ≠ x), Membership.mem (γ := Set X) (closure[inst] {x}ᶜ) y
⊢ Membership.mem (γ := Set X) (closure[inst] {x}ᶜ) y

Tactic:
rcases eq_or_ne y x with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
y : X
inst_1 inl inl₁ inl₂ inl₃ : (𝓝[≠] y).NeBot
⊢ Membership.mem (γ := Set X) (closure[inst] {y}ᶜ) y

Tactic:
rwa [mem_closure_iff_nhdsWithin_neBot]

Premises used: mem_closure_iff_nhdsWithin_neBot
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
y : X
hne : y ≠ x
⊢ Membership.mem (γ := Set X) (closure[inst] {x}ᶜ) y

Tactic:
subset_closure hne

Premises used: subset_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
y : X
hne : y ≠ x
⊢ Membership.mem (γ := Set X) (closure[inst] {x}ᶜ) y

Tactic:
exact subset_closure hne

Premises used: subset_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
⊢ Eq (α := Set X) (closure[inst] {x}ᶜ) univ

Tactic:
(dense_compl_singleton x).closure_eq

Premises used: Dense.closure_eq, dense_compl_singleton
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
⊢ Eq (α := Set X) (interior {x}) ∅

Tactic:
interior_eq_empty_iff_dense_compl.2 (dense_compl_singleton x)

Premises used: Iff.mpr, dense_compl_singleton, interior_eq_empty_iff_dense_compl
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
⊢ ¬IsOpen[inst] {x}

Tactic:
dense_compl_singleton_iff_not_open.1 (dense_compl_singleton x)

Premises used: dense_compl_singleton_iff_not_open, dense_compl_singleton, Iff.mp
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s = {a : X | ClusterPt a (𝓟 s)}

Tactic:
Set.ext fun _ => mem_closure_iff_clusterPt

Premises used: Set.ext, mem_closure_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst] s ↔ ∀ t ∈ 𝓝 x, (t ∩ s).Nonempty

Tactic:
mem_closure_iff_clusterPt.trans clusterPt_principal_iff

Premises used: clusterPt_principal_iff, mem_closure_iff_clusterPt, Iff.trans
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst] s ↔ ∀ t ∈ 𝓝 x, ∃ (y : (↑s : Type u)), (↑y : X) ∈ t

Tactic:
simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]

Premises used: mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
simp_rw :
  (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
simp_rw₁ : (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ ∀ t ∈ 𝓝 x, ∃ (a : { x : X // x ∈ s }), (↑a : X) ∈ t
simp_rw₂ : (∀ t ∈ 𝓝 x, ∃ x ∈ s, x ∈ t) ↔ ∀ t ∈ 𝓝 x, ∃ (a : { x : X // x ∈ s }), (↑a : X) ∈ t
simp_rw₃ : (∀ t ∈ 𝓝 x, ∃ x ∈ s, x ∈ t) ↔ ∀ t ∈ 𝓝 x, ∃ (x : X) (_ : x ∈ s), x ∈ t
⊢ x ∈ closure[inst] s ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))

Tactic:
simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]

Premises used: mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop, Filter.comap_neBot_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort w
x : X
t : Set X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (∀ ⦃i : ι⦄, p i → ∀ ⦃j : Unit⦄, True → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty

Tactic:
simp only [forall_const]

Premises used: forall_const
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort w
x : X
t : Set X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (∀ (i : ι), p i → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i

Tactic:
simp only [Set.Nonempty, mem_inter_iff, and_comm]

Premises used: Set.mem_inter_iff, and_comm, Set.Nonempty
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
simp_rw : (∀ s ∈ F, x ∈ closure[inst] s) ↔ pure x ≤ F.lift' closure[inst]
simp_rw₁ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] (id i')
simp_rw₂ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ {x} ⊆ closure[inst] i'
simp_rw₃ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), True ∧ x ∈ closure[inst] i'
simp_rw₄ : (∀ s ∈ F, x ∈ closure[inst] s) ↔ ∀ i' ∈ F, ∃ (i : Unit), x ∈ closure[inst] i'
⊢ ClusterPt x F ↔ pure x ≤ F.lift' closure[inst]

Tactic:
simp_rw [clusterPt_iff_forall_mem_closure,
    (hasBasis_pure _).le_basis_iff F.basis_sets.lift'_closure, id, singleton_subset_iff, true_and,
    exists_const]

Premises used: Set.singleton_subset_iff, Filter.hasBasis_pure, Filter.HasBasis.le_basis_iff, id, Filter.basis_sets, clusterPt_iff_forall_mem_closure, exists_const, Filter.HasBasis.lift'_closure, true_and
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : pure x ≤ F.lift' closure[inst] ↔ (pure x ⊓ F.lift' closure[inst]).NeBot
⊢ ClusterPt x F ↔ (F.lift' closure[inst] ⊓ pure x).NeBot

Tactic:
rw [clusterPt_iff_lift'_closure, inf_comm]

Premises used: inf_comm, clusterPt_iff_lift'_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
mp : pure x ≤ F.lift' closure[inst] → (pure x ⊓ F.lift' closure[inst]).NeBot
mpr : (pure x ⊓ F.lift' closure[inst]).NeBot → pure x ≤ F.lift' closure[inst]
⊢ pure x ≤ F.lift' closure[inst] ↔ (pure x ⊓ F.lift' closure[inst]).NeBot

Tactic:
constructor
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
h : pure x ≤ F.lift' closure[inst]
⊢ (pure x ⊓ F.lift' closure[inst]).NeBot

Tactic:
simp [h, pure_neBot]

Premises used: Filter.pure_neBot
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst]).NeBot
U : Set X
hU : U ∈ F.lift' closure[inst]
⊢ ∀ (s : Set X),
    (∃ (t₁ : Set X), Membership.mem (γ := Filter X) (pure x) t₁ ∧ ∃ t₂ ∈ F.lift' closure[inst], s = t₁ ∩ t₂) →
      s.Nonempty

Tactic:
simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h

Premises used: Filter.forall_mem_nonempty_iff_neBot, Filter.mem_inf_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure[inst]
h :
  ∀ (s : Set X),
    (∃ (t₁ : Set X), Membership.mem (γ := Filter X) (pure x) t₁ ∧ ∃ t₂ ∈ F.lift' closure[inst], s = t₁ ∩ t₂) →
      s.Nonempty
⊢ Membership.mem (γ := Filter X) (pure x) {x}

Tactic:
simp
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure[inst]
h :
  ∀ (s : Set X),
    (∃ (t₁ : Set X), Membership.mem (γ := Filter X) (pure x) t₁ ∧ ∃ t₂ ∈ F.lift' closure[inst], s = t₁ ∩ t₂) →
      s.Nonempty
⊢ Membership.mem (γ := Filter X) (pure x) U

Tactic:
simpa using h ({x} ∩ U) ⟨{x}, by simp, U, hU, rfl⟩

Premises used: Inter.inter, And.intro, Exists.intro, Singleton.singleton, rfl
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x (F.lift' closure[inst]) ↔ ClusterPt x F

Tactic:
simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)]

Premises used: clusterPt_iff_lift'_closure, Filter.lift'_lift'_assoc, monotone_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s ⊆ s ↔ ∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s

Tactic:
simp only [subset_def, mem_closure_iff_clusterPt]

Premises used: Set.subset_def, mem_closure_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[inst] s ↔ ∀ (a : X), AccPt a (𝓟 s) → a ∈ s

Tactic:
simp [isClosed_iff_clusterPt, clusterPt_principal, or_imp]

Premises used: or_imp, isClosed_iff_clusterPt, clusterPt_principal
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
simp_rw : (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
simp_rw₁ : (∀ (a : X), (𝓝 a ⊓ 𝓟 s).NeBot → a ∈ s) ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s
⊢ IsClosed[inst] s ↔ ∀ (x : X), (∀ U ∈ 𝓝 x, (U ∩ s).Nonempty) → x ∈ s

Tactic:
simp_rw [isClosed_iff_clusterPt, ClusterPt, inf_principal_neBot_iff]

Premises used: ClusterPt, isClosed_iff_clusterPt, Filter.inf_principal_neBot_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
simp_rw : (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
⊢ IsClosed[inst] s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
simp_rw [isClosed_iff_clusterPt]

Premises used: isClosed_iff_clusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
         fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩

Premises used: Filter.NeBot.mono, inf_le_right, nhds, le_inf, Iff.intro, Filter.principal, inf_le_left, Min.min
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ (∀ (a : X), ClusterPt a (𝓟 s) → a ∈ s) ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s

Tactic:
exact ⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS),
         fun hs x hx ↦ hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : x ∈ closure[inst] (s₁ ∪ s₂)
h₁ : s₁ᶜ ∈ 𝓝 x
rw : ∀ (h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
⊢ x ∈ closure[inst] s₂

Tactic:
rw [mem_closure_iff_nhds_ne_bot] at *

Premises used: mem_closure_iff_nhds_ne_bot
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 (s₁ ∪ s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
rwa : ∀ (h : 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂) ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
rwa₁ : ∀ (h : 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
rwa₂ : ∀ (h : ⊥ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥) (h₁ : s₁ᶜ ∈ 𝓝 x), 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥

Tactic:
rwa [← sup_principal, inf_sup_left, inf_principal_eq_bot.mpr h₁, bot_sup_eq] at h

Premises used: Iff.mpr, Filter.sup_principal, Filter.inf_principal_eq_bot, bot_sup_eq, inf_sup_left
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
t : Set X
hS : IsCoherentWith S
⊢ IsOpen[inst] t ↔ ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)

Tactic:
⟨fun ht _ _ ↦ ht.preimage continuous_subtype_val, hS.1 t⟩

Premises used: continuous_subtype_val, Topology.IsCoherentWith.isOpen_of_forall_induced, Iff.intro, IsOpen.preimage
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
t : Set X
hS : IsCoherentWith S
⊢ IsClosed[inst] t ↔ ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)

Tactic:
simp only [← isOpen_compl_iff, hS.isOpen_iff, preimage_compl]

Premises used: Set.preimage_compl, isOpen_compl_iff, Topology.IsCoherentWith.isOpen_iff
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
Y : Type u_2
inst_1 : TopologicalSpace Y
f : X → Y
hS : IsCoherentWith S
⊢ Continuous[inst, inst_1] f ↔ ∀ s ∈ S, ContinuousOn f s

Tactic:
⟨fun h _ _ ↦ h.continuousOn, fun h ↦ continuous_def.2 fun _u hu ↦ hS.isOpen_iff.2 fun s hs ↦
    hu.preimage <| (h s hs).restrict⟩

Premises used: Iff.mpr, Continuous.continuousOn, ContinuousOn.restrict, Iff.intro, IsOpen.preimage, continuous_def, Topology.IsCoherentWith.isOpen_iff