awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure s \ interior s ⊆ s ↔ IsClosed s
rw₁ : closure s ⊆ interior s ∪ s ↔ IsClosed s
rw₂ : closure s ⊆ s ↔ IsClosed s
rw₃ rw₄ : IsClosed s ↔ IsClosed s
⊢ frontier s ⊆ s ↔ IsClosed s

Tactic:
rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]

Premises used: Iff.mpr, frontier, interior_subset, closure_subset_iff_isClosed, Set.diff_subset_iff, Set.union_eq_right
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ frontier (closure s) ⊆ frontier s

Tactic:
diff_subset_diff closure_closure.subset <| interior_mono subset_closure

Premises used: frontier, Set.diff_subset_diff, interior_mono, subset_closure, Eq.subset, closure_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ frontier (interior s) ⊆ frontier s

Tactic:
diff_subset_diff (closure_mono interior_subset) interior_interior.symm.subset

Premises used: frontier, Set.diff_subset_diff, interior_subset, closure_mono, Eq.subset, interior_interior, Eq.symm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = frontier s

Tactic:
simp only [frontier_eq_closure_inter_closure, compl_compl, inter_comm]

Premises used: compl_compl, Set.inter_comm, frontier_eq_closure_inter_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq.{u + 1} (α := Set X) (frontier univ) ∅

Tactic:
simp [frontier]

Premises used: frontier
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq.{u + 1} (α := Set X) (frontier ∅) ∅

Tactic:
simp [frontier]

Premises used: frontier
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
simp :
  closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
⊢ frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

Tactic:
simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]

Premises used: Set.compl_inter, closure_union, frontier_eq_closure_inter_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)

Tactic:
(inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_

Premises used: LE.le.trans_eq, closure_inter_subset_inter_closure, Set.inter_subset_inter_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
refine :
  closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) =
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
⊢ closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)

Tactic:
refine (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_

Premises used: LE.le.trans_eq, closure_inter_subset_inter_closure, Set.inter_subset_inter_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) =
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)

Tactic:
simp only [inter_union_distrib_left, inter_assoc,
    inter_comm (closure t)]

Premises used: Set.inter_comm, closure, Set.inter_assoc, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t

Tactic:
simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᶜ tᶜ

Premises used: frontier_compl, Set.compl_union, Compl.compl, frontier_inter_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed s
rw : closure s \ interior s = s \ interior s
rw₁ rw₂ : s \ interior s = s \ interior s
⊢ frontier s = s \ interior s

Tactic:
rw [frontier, hs.closure_eq]

Premises used: frontier, IsClosed.closure_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen s
rw : closure s \ interior s = closure s \ s
rw₁ rw₂ : closure s \ s = closure s \ s
⊢ frontier s = closure s \ s

Tactic:
rw [frontier, hs.interior_eq]

Premises used: frontier, IsOpen.interior_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen s
rw : s ∩ (closure s \ s) = ∅
rw₁ rw₂ : Eq.{u + 1} (α := Set X) ∅ ∅
⊢ s ∩ frontier s = ∅

Tactic:
rw [hs.frontier_eq, inter_diff_self]

Premises used: Set.inter_diff_self, IsOpen.frontier_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : Disjoint (frontier s) s ↔ IsClosed sᶜ
rw₁ : Disjoint (frontier s) s ↔ frontier sᶜ ⊆ sᶜ
rw₂ : Disjoint (frontier s) s ↔ frontier s ⊆ sᶜ
rw₃ rw₄ : Disjoint (frontier s) s ↔ Disjoint (frontier s) s
⊢ Disjoint (frontier s) s ↔ IsOpen s

Tactic:
rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
    frontier_compl, subset_compl_iff_disjoint_right]

Premises used: frontier_compl, frontier_subset_iff_isClosed, Set.subset_compl_iff_disjoint_right, isClosed_compl_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : IsClosed (closure s ∩ closure sᶜ)
⊢ IsClosed (frontier s)

Tactic:
rw [frontier_eq_closure_inter_closure]

Premises used: frontier_eq_closure_inter_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)

Tactic:
IsClosed.inter isClosed_closure isClosed_closure

Premises used: IsClosed.inter, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)

Tactic:
exact IsClosed.inter isClosed_closure isClosed_closure

Premises used: IsClosed.inter, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
⊢ frontier s = s \ interior s

Tactic:
have A : frontier s = s \ interior s := h.frontier_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
rw : interior (s \ interior s) ⊆ interior s
⊢ interior (frontier s) ⊆ interior s

Tactic:
rw [A]
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s

Tactic:
interior_mono diff_subset

Premises used: Set.diff_subset, interior_mono
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (s \ interior s) ⊆ interior s

Tactic:
exact interior_mono diff_subset

Premises used: Set.diff_subset, interior_mono
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) ⊆ interior s

Tactic:
have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono diff_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
⊢ interior (frontier s) ⊆ frontier s

Tactic:
have C : interior (frontier s) ⊆ frontier s := interior_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) ⊆ s \ interior s

Tactic:
simpa [A] using C
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) ⊆ interior s ∩ (s \ interior s)

Tactic:
have : interior (frontier s) ⊆ interior s ∩ (s \ interior s) :=
    subset_inter B (by simpa [A] using C)
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
rwa : ∀ (this : interior (frontier s) ⊆ ∅), interior (frontier s) = ∅
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : interior (frontier s) = ∅), interior (frontier s) = ∅
⊢ interior (frontier s) = ∅

Tactic:
rwa [inter_diff_self, subset_empty_iff] at this

Premises used: Set.inter_diff_self, Set.subset_empty_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s = interior s ∪ frontier s

Tactic:
(union_diff_cancel interior_subset_closure).symm

Premises used: frontier, Set.union_diff_cancel, interior_subset_closure, Eq.symm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s = s ∪ frontier s

Tactic:
(union_diff_cancel' interior_subset subset_closure).symm

Premises used: frontier, interior_subset, subset_closure, Eq.symm, Set.union_diff_cancel'
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
ht : IsOpen t
hd : Disjoint s t
⊢ Disjoint (frontier s) t

Tactic:
subset_compl_iff_disjoint_right.1 <|
    frontier_subset_closure.trans <| closure_minimal (disjoint_left.1 hd) <| isClosed_compl_iff.2 ht

Premises used: Iff.mpr, closure_minimal, Set.subset_compl_iff_disjoint_right, Set.disjoint_left, HasSubset.Subset.trans, Iff.mp, frontier_subset_closure, isClosed_compl_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsOpen s
hd : Disjoint s t
⊢ Disjoint s (frontier t)

Tactic:
(hd.symm.frontier_left hs).symm

Premises used: Disjoint.symm, Disjoint.frontier_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : frontier sᶜ = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
rw₁ : frontier sᶜ = closure sᶜ ∩ (interior sᶜ)ᶜ
rw₂ : frontier sᶜ = closure sᶜ \ interior sᶜ
rw₃ rw₄ : frontier sᶜ = frontier sᶜ
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ

Tactic:
rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]

Premises used: frontier_compl, Set.diff_eq, closure_compl, closure_diff_interior
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ
⊢ (frontier s)ᶜ = interior s ∪ interior sᶜ

Tactic:
rw [frontier_eq_inter_compl_interior]

Premises used: frontier_eq_inter_compl_interior
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ

Tactic:
simp only [compl_inter, compl_compl]

Premises used: compl_compl, Set.compl_inter
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ ClusterPt x ⊤

Tactic:
simp [ClusterPt]

Premises used: ClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F G : Filter X
⊢ ClusterPt x (F ⊔ G) ↔ ClusterPt x F ∨ ClusterPt x G

Tactic:
simp only [ClusterPt, inf_sup_left, sup_neBot]

Premises used: ClusterPt, inf_sup_left, Filter.sup_neBot
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
h : ClusterPt x F
⊢ (𝓝 x ⊓ F).NeBot

Tactic:
h

Premises used: ClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ιX : Sort u_3
ιF : Sort u_4
pX : ιX → Prop
sX : ιX → Set X
pF : ιF → Prop
sF : ιF → Set X
F : Filter X
hX : (𝓝 x).HasBasis pX sX
hF : F.HasBasis pF sF
⊢ ClusterPt x F ↔ ∀ ⦃i : ιX⦄, pX i → ∀ ⦃j : ιF⦄, pF j → (sX i ∩ sF j).Nonempty

Tactic:
hX.inf_basis_neBot_iff hF

Premises used: Filter.HasBasis.inf_basis_neBot_iff, ClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : (𝓝 x).HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in F, x ∈ s i

Tactic:
simp only [hx.clusterPt_iff F.basis_sets, Filter.frequently_iff, inter_comm (s _),
    Set.Nonempty, id, mem_inter_iff]

Premises used: Filter.frequently_iff, Set.mem_inter_iff, id, Filter.basis_sets, Set.inter_comm, Set.Nonempty, Filter.HasBasis.clusterPt_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ∀ s ∈ 𝓝 x, ∃ᶠ (y : X) in F, y ∈ s

Tactic:
(𝓝 x).basis_sets.clusterPt_iff_frequently

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

Tactic:
clusterPt_iff_frequently.mp hx {y | p y} hp

Premises used: Set.Mem, setOf, clusterPt_iff_frequently, Iff.mp
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
simp :
  (∀ ⦃i : Set X⦄, i ∈ 𝓝 x → ∀ ⦃j : ι⦄, p j → (id i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ {U : Set X}, U ∈ 𝓝 x → ∃ x ∈ U, x ∈ s i
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in 𝓝 x, x ∈ s i

Tactic:
simp only [(𝓝 x).basis_sets.clusterPt_iff hx, Filter.frequently_iff]

Premises used: Filter.frequently_iff, nhds, Filter.basis_sets, Filter.HasBasis.clusterPt_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ (∀ ⦃i : Set X⦄, i ∈ 𝓝 x → ∀ ⦃j : ι⦄, p j → (id i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ {U : Set X}, U ∈ 𝓝 x → ∃ x ∈ U, x ∈ s i

Tactic:
⟨fun h a b c d ↦ h d b, fun h a b c d ↦ h c d b⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ (∀ ⦃i : Set X⦄, i ∈ 𝓝 x → ∀ ⦃j : ι⦄, p j → (id i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ {U : Set X}, U ∈ 𝓝 x → ∃ x ∈ U, x ∈ s i

Tactic:
exact ⟨fun h a b c d ↦ h d b, fun h a b c d ↦ h c d b⟩
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ∀ s ∈ F, ∃ᶠ (y : X) in 𝓝 x, y ∈ s

Tactic:
F.basis_sets.clusterPt_iff_frequently'

Premises used: Filter.HasBasis.clusterPt_iff_frequently', Set.Mem, Filter.basis_sets
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
p : X → Prop
hx : ClusterPt x F
hp : ∀ᶠ (y : X) in F, p y
⊢ ∃ᶠ (y : X) in 𝓝 x, p y

Tactic:
clusterPt_iff_frequently'.mp hx {y | p y} hp

Premises used: Set.Mem, clusterPt_iff_frequently', setOf, Iff.mp
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ 𝓝 x → ∀ ⦃V : Set X⦄, V ∈ F → (U ∩ V).Nonempty

Tactic:
inf_neBot_iff

Premises used: ClusterPt, Filter.inf_neBot_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : ClusterPt x F ↔ ¬𝓝 x ⊓ F = ⊥
rw₁ : (𝓝 x ⊓ F).NeBot ↔ ¬𝓝 x ⊓ F = ⊥
rw₂ rw₃ : 𝓝 x ⊓ F ≠ ⊥ ↔ ¬𝓝 x ⊓ F = ⊥
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F

Tactic:
rw [disjoint_iff, ClusterPt, neBot_iff]

Premises used: disjoint_iff, Filter.neBot_iff, ClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
simp :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → x ∈ closure[inst] (s i)

Tactic:
simp only [(nhds_basis_opens _).clusterPt_iff hF, mem_closure_iff]

Premises used: mem_closure_iff, Filter.HasBasis.clusterPt_iff, nhds_basis_opens
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
mp :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
mp₁ mp₂ mp₃ :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr₁ mpr₂ mpr₃ :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
mp₄ mp₅ mp₆ :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr₄ mpr₅ mpr₆ :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i → IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
mp₇ mp₈ mp₉ :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr₇ mpr₈ mpr₉ :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i → IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
mp₁₀ mp₁₁ mp₁₂ :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr₁₀ mpr₁₁ mpr₁₂ :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i → IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
mp₁₃ mp₁₄ :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr₁₃ mpr₁₄ :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i → IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
⊢ (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty

Tactic:
tauto
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ∀ s ∈ F, x ∈ closure[inst] s

Tactic:
F.basis_sets.clusterPt_iff_forall_mem_closure

Premises used: Set.Mem, Filter.basis_sets, Filter.HasBasis.clusterPt_iff_forall_mem_closure
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ ClusterPt x (𝓟 s) ↔ ∀ U ∈ 𝓝 x, (U ∩ s).Nonempty

Tactic:
inf_principal_neBot_iff

Premises used: ClusterPt, Filter.inf_principal_neBot_iff
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ ClusterPt x (𝓟 s) ↔ ∃ᶠ (y : X) in 𝓝 x, y ∈ s

Tactic:
simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, mem_inter_iff]

Premises used: clusterPt_principal_iff, Filter.frequently_iff, Set.mem_inter_iff, Set.Nonempty
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst_1 : f.NeBot
rwa : (𝓝 x ⊓ f).NeBot
rwa₁ rwa₂ rwa₃ rwa₄ : f.NeBot
⊢ ClusterPt x f

Tactic:
rwa [ClusterPt, inf_eq_right.mpr H]

Premises used: Iff.mpr, ClusterPt, inf_eq_right
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
_hf : f.NeBot
⊢ ClusterPt x f

Tactic:
ClusterPt.of_le_nhds H

Premises used: ClusterPt.of_le_nhds
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f : Filter X
H : 𝓝 x ≤ f
⊢ ClusterPt x f

Tactic:
simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]

Premises used: Iff.mpr, nhds_neBot, ClusterPt, inf_eq_left
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f g : Filter X
H : ClusterPt x f
h : f ≤ g
⊢ ClusterPt x g

Tactic:
NeBot.mono H <| inf_le_inf_left _ h

Premises used: Filter.NeBot.mono, inf_le_inf_left, ClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f g : Filter X
H : ClusterPt x (f ⊓ g)
⊢ ClusterPt x f

Tactic:
H.mono inf_le_left

Premises used: ClusterPt.mono, inf_le_left
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f g : Filter X
H : ClusterPt x (f ⊓ g)
⊢ ClusterPt x g

Tactic:
H.mono inf_le_right

Premises used: ClusterPt.mono, inf_le_right
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
⊢ MapClusterPt x F u ↔ ClusterPt x (map u F)

Tactic:
Iff.rfl

Premises used: Iff.rfl, MapClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
v : α → X
h : u =ᶠ[F] v
⊢ MapClusterPt x F u ↔ MapClusterPt x F v

Tactic:
simp only [mapClusterPt_def, map_congr h]

Premises used: mapClusterPt_def, Filter.map_congr
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
G : Filter α
h : MapClusterPt x F u
hle : F ≤ G
⊢ MapClusterPt x G u

Tactic:
h.clusterPt.mono (map_mono hle)

Premises used: Filter.map_mono, ClusterPt.mono, MapClusterPt.clusterPt, MapClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
α : Type u_1
F : Filter α
u : α → X
x : X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (𝓝 x ⊓ map u F) (𝓝 y)
hu : MapClusterPt x F u
⊢ MapClusterPt y F (f ∘ u)

Tactic:
(tendsto_inf.2 ⟨hf, tendsto_map.mono_left inf_le_right⟩).neBot (hx := hu)

Premises used: Iff.mpr, Filter.tendsto_inf, Set.Mem, setOf, inf_le_right, ClusterPt, Filter.tendsto_map, Set.preimage, And.intro, MapClusterPt, Filter.Tendsto.mono_left, Filter.Tendsto.neBot
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
α : Type u_1
F : Filter α
u : α → X
x : X
inst_1 : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (𝓝 x) (𝓝 y)
hu : MapClusterPt x F u
⊢ MapClusterPt y F (f ∘ u)

Tactic:
hu.tendsto_comp' (hf.mono_left inf_le_left)

Premises used: MapClusterPt.tendsto_comp', Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Topology.ClusterPt
Goal:
α : Type u_1
F : Filter α
inst : TopologicalSpace α
a : α
rw : ClusterPt a (map id F) ↔ ClusterPt a F
rw₁ rw₂ : ClusterPt a F ↔ ClusterPt a F
⊢ MapClusterPt a F id ↔ ClusterPt a F

Tactic:
rw [MapClusterPt, map_id]

Premises used: Filter.map_id, MapClusterPt
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
Y : Type v
α : Type u_1
F : Filter α
u : α → X
x : X
inst_1 : TopologicalSpace Y
f : X → Y
hf : ContinuousAt f x
hu : MapClusterPt x F u
⊢ MapClusterPt (f x) F (f ∘ u)

Tactic:
hu.tendsto_comp hf

Premises used: MapClusterPt.tendsto_comp
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
inst_1 : TopologicalSpace α
a : α
hf : ContinuousAt u a
hu : ClusterPt a F
⊢ MapClusterPt (u a) F u

Tactic:
hu.mapClusterPt_id.continuousAt_comp hf

Premises used: ClusterPt.mapClusterPt_id, MapClusterPt.continuousAt_comp
-- Module: Mathlib.Topology.ClusterPt
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
simp_rw : ClusterPt x (Filter.map u F) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
simp_rw₁ : (∀ (i : ι), p i → ∃ᶠ (x : X) in Filter.map u F, x ∈ s i) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
⊢ MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i

Tactic:
simp_rw [MapClusterPt, hx.clusterPt_iff_frequently, frequently_map]

Premises used: Filter.HasBasis.clusterPt_iff_frequently, Filter.frequently_map, MapClusterPt