awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h_1 : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
s t : Clopens X
h :
  ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))) =
    ⋯.choose (p := fun (t_1 : Finset (↑(countableBasis X) : Type u_1)) ↦
      t.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t_1 : Set (↑(countableBasis X) : Type u_1))))
h₁ : (↑s : Set X) = (↑t : Set X)
⊢ s = t

Tactic:
ext1
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
⊢ Injective f

Tactic:
have hf : f.Injective := by
      intro s t (h : Exists.choose _ = Exists.choose _)
      ext1; change s.carrier = t.carrier
      rw [(this s).choose_spec, (this t).choose_spec, h]
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
hf : Injective f
⊢ Countable.{u_1 + 1} (Clopens X)

Tactic:
hf.countable

Premises used: Function.Injective.countable
-- Module: Mathlib.Topology.ClopenBox
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : T2Space X
inst_3 : TotallyDisconnectedSpace X
h : SecondCountableTopology X
this :
  ∀ (s : Clopens X),
    ∃ (t : Finset (↑(countableBasis X) : Type u_1)),
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1)))
f : Clopens X → Finset (↑(countableBasis X) : Type u_1) :=
  fun (s : Clopens X) ↦
    ⋯.choose (p := fun (t : Finset (↑(countableBasis X) : Type u_1)) ↦
      s.carrier =
        ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ countableBasis X) '' (↑t : Set (↑(countableBasis X) : Type u_1))))
hf : Injective f
⊢ Countable.{u_1 + 1} (Clopens X)

Tactic:
exact hf.countable

Premises used: Function.Injective.countable
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
simp only [interior, mem_sUnion, mem_setOf_eq, and_assoc, and_left_comm]

Premises used: and_left_comm, Set.mem_setOf_eq, interior, and_assoc, Set.mem_sUnion
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsOpen (interior s)

Tactic:
isOpen_sUnion fun _ => And.left

Premises used: And.left, interior, isOpen_sUnion
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior s ⊆ s

Tactic:
sUnion_subset fun _ => And.right

Premises used: Set.sUnion_subset, And.right, interior
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h₁ : t ⊆ s
h₂ : IsOpen t
⊢ t ⊆ interior s

Tactic:
subset_sUnion_of_mem ⟨h₂, h₁⟩

Premises used: And.intro, interior, Set.subset_sUnion_of_mem
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsOpen s
⊢ interior s = s

Tactic:
interior_subset.antisymm (interior_maximal (Subset.refl s) h)

Premises used: Set.Subset.refl, interior_subset, interior_maximal, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
p : Set X → Prop
⊢ (∀ (t : Set X), IsOpen t → p t) ↔ ∀ (t : Set X), p (interior t)

Tactic:
⟨fun h t ↦ h (interior t) isOpen_interior, fun h t ht ↦ ht.interior_eq ▸ h t⟩

Premises used: isOpen_interior, Eq.rec, interior, Iff.intro, IsOpen.interior_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
p : Set X → Prop
⊢ (∃ (t : Set X), IsOpen t ∧ p t) ↔ ∃ (t : Set X), p (interior t)

Tactic:
⟨fun ⟨_, h⟩ ↦ ⟨_, h.1.interior_eq ▸ h.2⟩, fun ⟨_, h⟩ ↦ ⟨_, isOpen_interior, h⟩⟩

Premises used: isOpen_interior, Exists, And, _private.0.exists_isOpen_iff.match_2, And.intro, interior, Iff.intro, Exists.intro, IsOpen, _private.0.exists_isOpen_iff.match_1
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior s = s ↔ IsOpen s

Tactic:
⟨fun h => h ▸ isOpen_interior, IsOpen.interior_eq⟩

Premises used: isOpen_interior, Eq.rec, Iff.intro, IsOpen.interior_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ IsOpen s

Tactic:
simp only [interior_eq_iff_isOpen.symm, Subset.antisymm_iff, interior_subset, true_and]

Premises used: interior_subset, Set.Subset.antisymm_iff, interior_eq_iff_isOpen, Iff.symm, true_and
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h₁ : IsOpen s
⊢ s ⊆ interior t ↔ s ⊆ t

Tactic:
⟨fun h => Subset.trans h interior_subset, fun h₂ => interior_maximal h₂ h₁⟩

Premises used: interior_subset, Set.Subset.trans, interior_maximal, Iff.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ t ⊆ interior s ↔ ∃ (U : Set X), IsOpen U ∧ t ⊆ U ∧ U ⊆ s

Tactic:
⟨fun h => ⟨interior s, isOpen_interior, h, interior_subset⟩, fun ⟨_U, hU, htU, hUs⟩ =>
    htU.trans (interior_maximal hUs hU)⟩

Premises used: interior_subset, isOpen_interior, interior_maximal, HasSubset.Subset.trans, HasSubset.Subset, _private.0.subset_interior_iff.match_1, And.intro, interior, Iff.intro, Exists.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ interior s ⊆ t ↔ ∀ (U : Set X), IsOpen U → U ⊆ s → U ⊆ t

Tactic:
simp [interior]

Premises used: interior
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : s ⊆ t
⊢ interior s ⊆ interior t

Tactic:
interior_maximal (Subset.trans interior_subset h) isOpen_interior

Premises used: interior_subset, Set.Subset.trans, isOpen_interior, interior_maximal
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ interior s ∪ interior t ⊆ interior (s ∪ t)

Tactic:
union_subset (interior_mono subset_union_left) (interior_mono subset_union_right)

Premises used: interior_mono, Set.subset_union_right, Set.union_subset, Set.subset_union_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq.{u + 1} (α := Set X) (interior ∅) ∅

Tactic:
isOpen_empty.interior_eq

Premises used: IsOpen.interior_eq, isOpen_empty
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq.{u + 1} (α := Set X) (interior univ) univ

Tactic:
isOpen_univ.interior_eq

Premises used: isOpen_univ, IsOpen.interior_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior s = univ ↔ s = univ

Tactic:
⟨fun h => univ_subset_iff.mp <| h.symm.trans_le interior_subset, fun h => h.symm ▸ interior_univ⟩

Premises used: Set.univ_subset_iff, interior_subset, interior_univ, Eq.rec, Eq.trans_le, Iff.intro, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior (interior s) = interior s

Tactic:
isOpen_interior.interior_eq

Premises used: isOpen_interior, IsOpen.interior_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ interior (s ∩ t) = interior s ∩ interior t

Tactic:
(Monotone.map_inf_le (fun _ _ ↦ interior_mono) s t).antisymm <|
    interior_maximal (inter_subset_inter interior_subset interior_subset) <|
      isOpen_interior.inter isOpen_interior

Premises used: interior_subset, interior_mono, isOpen_interior, interior_maximal, LE.le.antisymm, Set.inter_subset_inter, IsOpen.inter, Monotone.map_inf_le
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Set ι
f : ι → Set X
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), f i))
    (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), interior (f i))

Tactic:
simp
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Set ι
f : ι → Set X
a : ι
s_1 : Set ι
h : a ∉ s_1
hs : s_1.Finite
h_1 : Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ s_1, f i)) (⋂ i ∈ s_1, interior (f i))
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ insert a s_1, f i)) (⋂ i ∈ insert a s_1, interior (f i))

Tactic:
simp [*]
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Set ι
hs : s.Finite
f : ι → Set X
empty :
  Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), f i))
    (⋂ (i : ι), ⋂ (_ : Membership.mem (γ := Set ι) ∅ i), interior (f i))
insert :
  ∀ {a : ι} {s : Set ι},
    a ∉ s →
      s.Finite →
        Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ s, f i)) (⋂ i ∈ s, interior (f i)) →
          Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ Insert.insert a s, f i)) (⋂ i ∈ Insert.insert a s, interior (f i))
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ s, f i)) (⋂ i ∈ s, interior (f i))

Tactic:
induction s, hs using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ _ => simp [*]

Premises used: Insert.insert
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
rw : Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ S, i)) (⋂ s ∈ S, interior s)
rw₁ rw₂ : Eq.{u + 1} (α := Set X) (⋂ i ∈ S, interior i) (⋂ s ∈ S, interior s)
⊢ interior (⋂₀ S) = ⋂ s ∈ S, interior s

Tactic:
rw [sInter_eq_biInter, hS.interior_biInter]

Premises used: Set.sInter_eq_biInter, Set.Finite.interior_biInter
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Finset ι
f : ι → Set X
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ s, f i)) (⋂ i ∈ s, interior (f i))

Tactic:
s.finite_toSet.interior_biInter f

Premises used: Set.Finite.interior_biInter, Finset.finite_toSet
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
inst_1 : Finite ι
f : ι → Set X
rw : interior (⋂₀ range f) = ⋂ (i : ι), interior (f i)
rw₁ : Eq.{u + 1} (α := Set X) (⋂ s ∈ range f, interior s) (⋂ (i : ι), interior (f i))
rw₂ rw₃ : Eq.{u + 1} (α := Set X) (⋂ (y : ι), interior (f y)) (⋂ (i : ι), interior (f i))
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), f i)) (⋂ (i : ι), interior (f i))

Tactic:
rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]

Premises used: Set.Finite.interior_sInter, Set.finite_range, Set.biInter_range, Set.sInter_range
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
f : ℕ → Set X
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ (m : ℕ), ⋂ (_ : m < n), f m)) (⋂ (m : ℕ), ⋂ (_ : m < n), interior (f m))

Tactic:
(finite_lt_nat n).interior_biInter f

Premises used: Set.Mem, Set.Finite.interior_biInter, Set.finite_lt_nat, Nat.lt
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
f : ℕ → Set X
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ (m : ℕ), ⋂ (_ : m ≤ n), f m)) (⋂ (m : ℕ), ⋂ (_ : m ≤ n), interior (f m))

Tactic:
(finite_le_nat n).interior_biInter f

Premises used: Set.Mem, setOf, Set.Finite.interior_biInter, Set.finite_le_nat
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ interior (s ∪ t) ∩ interior sᶜ ⊆ interior t

Tactic:
interior_inter.symm.trans_subset <| interior_mono (union_inter_compl_left_subset ..)

Premises used: interior_inter, interior_mono, Set.union_inter_compl_left_subset, Eq.symm, Eq.trans_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s

Tactic:
interior_inter.symm.trans_subset <| interior_mono (union_inter_compl_right_subset ..)

Premises used: interior_inter, interior_mono, Set.union_inter_compl_right_subset, Eq.symm, Eq.trans_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
h : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this rwa rwa₁ rwa₂ rwa₃ : u \ s ⊆ t
⊢ u \ s ⊆ interior t

Tactic:
rwa [(IsOpen.sdiff hu₁ h₁).subset_interior_iff]

Premises used: IsOpen.subset_interior_iff, IsOpen.sdiff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
h : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this_1 : u \ s ⊆ t
this : u \ s ⊆ interior t
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : u \ s ⊆ ∅), u \ s ⊆ ∅
⊢ u \ s ⊆ ∅

Tactic:
rwa [h₂] at this
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
rw [← subset_interior_iff_isOpen]

Premises used: subset_interior_iff_isOpen
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
simp only [subset_def, mem_interior]

Premises used: Set.subset_def, mem_interior
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
s : ι → Set X
⊢ Subset.{u} (α := Set X) (interior (⋂ (i : ι), s i)) (⋂ (i : ι), interior (s i))

Tactic:
subset_iInter fun _ => interior_mono <| iInter_subset _ _

Premises used: interior_mono, Set.subset_iInter, Set.iInter_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
p : ι → Sort u_1
s : (i : ι) → p i → Set X
⊢ Subset.{u} (α := Set X) (interior (⋂ (i : ι), ⋂ (j : p i), s i j)) (⋂ (i : ι), ⋂ (j : p i), interior (s i j))

Tactic:
(interior_iInter_subset _).trans <| iInter_mono fun _ => interior_iInter_subset _

Premises used: HasSubset.Subset.trans, interior_iInter_subset, Set.iInter_mono
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
rw rw₁ : Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ S, i)) (interior (⋂ s ∈ S, s))
⊢ interior (⋂₀ S) = interior (⋂ s ∈ S, s)

Tactic:
rw [sInter_eq_biInter]

Premises used: Set.sInter_eq_biInter
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
l : Filter X
p : ι → Prop
s : ι → Set X
h : l.HasBasis p s
⊢ (l.lift' interior).HasBasis p fun (i : ι) ↦ interior (s i)

Tactic:
h.lift' fun _ _ ↦ interior_mono

Premises used: interior_mono, Set.sUnion, interior, Filter.HasBasis.lift'
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
l : Filter X
⊢ l.lift' interior ≤ l

Tactic:
fun _s hs ↦
  mem_of_superset (mem_lift' hs) interior_subset

Premises used: interior_subset, Filter.mem_lift', Filter.mem_of_superset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
l : Filter X
p : ι → Prop
s : ι → Set X
h : l.HasBasis p s
ho : ∀ (i : ι), p i → IsOpen (s i)
i : ι
hi : p i
⊢ interior (s i) ∈ l

Tactic:
simpa only [(ho i hi).interior_eq] using h.mem_of_mem hi

Premises used: IsOpen.interior_eq, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s)

Tactic:
isClosed_sInter fun _ => And.left

Premises used: closure, And.left, isClosed_sInter
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ closure s

Tactic:
subset_sInter fun _ => And.right

Premises used: closure, And.right, Set.subset_sInter
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
P : X
hP : P ∉ closure s
⊢ P ∉ s

Tactic:
fun h =>
  hP (subset_closure h)

Premises used: subset_closure, Not
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsClosed t
⊢ closure s ⊆ t

Tactic:
sInter_subset_of_mem ⟨h₂, h₁⟩

Premises used: Set.sInter_subset_of_mem, closure, And.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hd : Disjoint s t
ht : IsOpen t
⊢ Disjoint (closure s) t

Tactic:
disjoint_compl_left.mono_left <| closure_minimal hd.subset_compl_right ht.isClosed_compl

Premises used: Disjoint.subset_compl_right, closure_minimal, disjoint_compl_left, IsOpen.isClosed_compl, Disjoint.mono_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hd : Disjoint s t
hs : IsOpen s
⊢ Disjoint s (closure t)

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

Premises used: Disjoint.symm, Disjoint.closure_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
⊢ closure s = s

Tactic:
Subset.antisymm (closure_minimal (Subset.refl s) h) subset_closure

Premises used: Set.Subset.antisymm, Set.Subset.refl, subset_closure, closure_minimal
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
p : Set X → Prop
⊢ (∀ (t : Set X), IsClosed t → p t) ↔ ∀ (t : Set X), p (closure t)

Tactic:
⟨fun h t ↦ h (closure t) isClosed_closure, fun h t ht ↦ ht.closure_eq ▸ h t⟩

Premises used: IsClosed.closure_eq, Eq.rec, closure, Iff.intro, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
p : Set X → Prop
⊢ (∃ (t : Set X), IsClosed t ∧ p t) ↔ ∃ (t : Set X), p (closure t)

Tactic:
⟨fun ⟨_, h⟩ ↦ ⟨_, h.1.closure_eq ▸ h.2⟩, fun ⟨_, h⟩ ↦ ⟨_, isClosed_closure, h⟩⟩

Premises used: _private.0.exists_isClosed_iff.match_1, Exists, IsClosed, And, closure, _private.0.exists_isClosed_iff.match_2, And.intro, Iff.intro, Exists.intro, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ closure s ⊆ s

Tactic:
closure_minimal (Subset.refl _) hs

Premises used: Set.Subset.refl, closure_minimal
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h₁ : IsClosed t
⊢ closure s ⊆ t ↔ s ⊆ t

Tactic:
⟨Subset.trans subset_closure, fun h => closure_minimal h h₁⟩

Premises used: Set.Subset.trans, subset_closure, closure_minimal, Iff.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
hs : IsClosed s
⊢ x ∈ s ↔ closure {x} ⊆ s

Tactic:
(hs.closure_subset_iff.trans Set.singleton_subset_iff).symm

Premises used: Set.singleton_subset_iff, IsClosed.closure_subset_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : s ⊆ t
⊢ closure s ⊆ closure t

Tactic:
closure_minimal (Subset.trans h subset_closure) isClosed_closure

Premises used: Set.Subset.trans, subset_closure, closure_minimal, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Monotone.{u_1, u_1} (α := Set X) closure

Tactic:
fun _ _ =>
  closure_mono

Premises used: Monotone, closure_mono
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure (s ∩ t) ⊆ closure s ∩ closure t

Tactic:
subset_inter (closure_mono inter_subset_left) (closure_mono inter_subset_right)

Premises used: Set.inter_subset_left, closure_mono, Set.subset_inter, Set.inter_subset_right
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
rw : s ⊆ t ∪ closure t ↔ s ⊆ closure t
rw₁ rw₂ : s ⊆ closure t ↔ s ⊆ closure t
⊢ s \ t ⊆ closure t ↔ s ⊆ closure t

Tactic:
rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]

Premises used: subset_closure, Set.diff_subset_iff, Set.union_eq_self_of_subset_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure (s ∩ t) ⊆ closure s ∩ closure t

Tactic:
(monotone_closure X).map_inf_le s t

Premises used: Monotone.map_inf_le, monotone_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : closure s ⊆ s
rw : IsClosed (closure s)
⊢ IsClosed s

Tactic:
rw [subset_closure.antisymm h]

Premises used: subset_closure, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)

Tactic:
isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed (closure s)

Tactic:
exact isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s = s ↔ IsClosed s

Tactic:
⟨fun h => h ▸ isClosed_closure, IsClosed.closure_eq⟩

Premises used: IsClosed.closure_eq, Eq.rec, Iff.intro, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s ⊆ s ↔ IsClosed s

Tactic:
⟨isClosed_of_closure_subset, IsClosed.closure_subset⟩

Premises used: IsClosed.closure_subset, Iff.intro, isClosed_of_closure_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq.{u + 1} (α := Set X) (closure ∅) ∅

Tactic:
isClosed_empty.closure_eq

Premises used: IsClosed.closure_eq, isClosed_empty
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s = ∅ ↔ s = ∅

Tactic:
⟨subset_eq_empty subset_closure, fun h => h.symm ▸ closure_empty⟩

Premises used: subset_closure, Eq.rec, Iff.intro, closure_empty, Eq.symm, Set.subset_eq_empty
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ (closure s).Nonempty ↔ s.Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, closure_empty_iff]

Premises used: closure_empty_iff, Ne, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Eq.{u + 1} (α := Set X) (closure univ) univ

Tactic:
isClosed_univ.closure_eq

Premises used: isClosed_univ, IsClosed.closure_eq
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure (closure s) = closure s

Tactic:
isClosed_closure.closure_eq

Premises used: IsClosed.closure_eq, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : Eq.{u + 1} (α := Set X) (⋂₀ {t : Set X | IsClosed t ∧ s ⊆ t}) (⋂₀ {s_1 : Set X | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ})
⊢ closure s = (interior sᶜ)ᶜ

Tactic:
rw [interior, closure, compl_sUnion, compl_image_set_of]

Premises used: Set.compl_image_set_of, closure, Set.compl_sUnion, interior
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ Eq.{u + 1} (α := Set X) (⋂₀ {t : Set X | IsClosed t ∧ s ⊆ t}) (⋂₀ {s_1 : Set X | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ})

Tactic:
simp only [compl_subset_compl, isOpen_compl_iff]

Premises used: Set.compl_subset_compl, isOpen_compl_iff