awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
s : Set X
h : x ⤳ y
hs : IsClosed[inst] s
hx : x ∈ s
⊢ y ∈ s

Tactic:
specializes_iff_forall_closed.1 h s hs hx

Premises used: Iff.mp, specializes_iff_forall_closed
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
s : Set X
hs : IsClosed[inst] s
hx : x ∈ s
hy : y ∉ s
⊢ ¬x ⤳ y

Tactic:
fun h =>
  hy <| h.mem_closed hs hx

Premises used: Not, Specializes.mem_closed
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ Membership.mem (γ := Set X) (closure[inst] {x}) y

Tactic:
(specializes_TFAE x y).out 0 4

Premises used: List.TFAE.out, OfNat.ofNat, specializes_TFAE
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ Subset (α := Set X) (closure[inst] {y}) (closure[inst] {x})

Tactic:
(specializes_TFAE x y).out 0 5

Premises used: List.TFAE.out, OfNat.ofNat, specializes_TFAE
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ ClusterPt y (pure x)

Tactic:
(specializes_TFAE x y).out 0 6

Premises used: List.TFAE.out, OfNat.ofNat, specializes_TFAE
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
ι : Sort u_7
p : ι → Prop
s : ι → Set X
h : (𝓝 y).HasBasis p s
⊢ x ⤳ y ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
specializes_iff_pure.trans h.ge_iff

Premises used: Filter.HasBasis.ge_iff, Iff.trans, specializes_iff_pure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ x ⤳ x

Tactic:
le_rfl

Premises used: le_rfl, Specializes
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ x ⤳ x

Tactic:
specializes_rfl

Premises used: specializes_rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
⊢ x ⤳ y → y ⤳ z → x ⤳ z

Tactic:
le_trans

Premises used: Specializes, le_trans
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
e : x = y
⊢ x ⤳ y

Tactic:
e ▸ specializes_refl x

Premises used: Eq.rec, specializes_refl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
s : Set X
h₁ : 𝓝[s] x ≤ 𝓝[s] y
h₂ : x ∈ s
⊢ x ⤳ y

Tactic:
specializes_iff_pure.2 <|
    calc
      pure x ≤ 𝓝[s] x := le_inf (pure_le_nhds _) (le_principal_iff.2 h₂)
      _ ≤ 𝓝[s] y := h₁
      _ ≤ 𝓝 y := inf_le_left

Premises used: Iff.mpr, Trans.trans, Filter.le_principal_iff, pure_le_nhds, le_inf, specializes_iff_pure, inf_le_left
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : x ⤳ y
hf : ContinuousWithinAt f s y
hx : x ∈ s
rw : ∀ (h : pure x ≤ 𝓝 y) (hf : ContinuousWithinAt f s y) (hx : x ∈ s), pure (f x) ≤ 𝓝 (f y)
⊢ f x ⤳ f y

Tactic:
rw [specializes_iff_pure] at h ⊢

Premises used: specializes_iff_pure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ pure (f x) = map f (pure x)

Tactic:
(map_pure f x).symm

Premises used: Eq.symm, Filter.map_pure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ map f (pure x) ≤ map f (𝓝 y ⊓ 𝓟 s)

Tactic:
map_mono (le_inf h ((pure_le_principal x).mpr hx))

Premises used: Iff.mpr, Filter.map_mono, le_inf, Filter.pure_le_principal
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ map f (𝓝 y ⊓ 𝓟 s) = map f (𝓝[s] y)

Tactic:
rfl

Premises used: nhdsWithin, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ map f (𝓝[s] y) ≤ 𝓝 (f y)

Tactic:
hf.tendsto

Premises used: Filter.Tendsto, ContinuousWithinAt.tendsto
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : pure x ≤ 𝓝 y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ pure (f x) ≤ 𝓝 (f y)

Tactic:
calc pure (f x)
    _ = map f (pure x) := (map_pure f x).symm
    _ ≤ map f (𝓝 y ⊓ 𝓟 s) := map_mono (le_inf h ((pure_le_principal x).mpr hx))
    _ = map f (𝓝[s] y) := rfl
    _ ≤ _ := hf.tendsto

Premises used: Pure.pure, Iff.mpr, Filter.map_mono, Filter.map, nhdsWithin, nhds, le_inf, Filter.pure_le_principal, Filter.principal, Eq.symm, Filter.map_pure, ContinuousWithinAt.tendsto, Min.min, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : x ⤳ y
hf : ContinuousOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f x ⤳ f y

Tactic:
h.map_of_continuousWithinAt (hf.continuousWithinAt hy) hx

Premises used: Specializes.map_of_continuousWithinAt, ContinuousOn.continuousWithinAt
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
h : x ⤳ y
hf : ContinuousAt f y
⊢ f x ⤳ f y

Tactic:
h.map_of_continuousWithinAt hf.continuousWithinAt (mem_univ x)

Premises used: ContinuousAt.continuousWithinAt, Specializes.map_of_continuousWithinAt, Set.mem_univ
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
h : x ⤳ y
hf : Continuous[inst, inst_1] f
⊢ f x ⤳ f y

Tactic:
h.map_of_continuousAt hf.continuousAt

Premises used: Specializes.map_of_continuousAt, Continuous.continuousAt
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x y : X
f : X → Y
hf : IsInducing f
⊢ f x ⤳ f y ↔ x ⤳ y

Tactic:
simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton,
    mem_preimage]

Premises used: Set.image_singleton, specializes_iff_mem_closure, Topology.IsInducing.closure_eq_preimage_closure_image, Set.mem_preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
p : X → Prop
x y : Subtype p
⊢ x ⤳ y ↔ (↑x : X) ⤳ (↑y : X)

Tactic:
IsInducing.subtypeVal.specializes_iff.symm

Premises used: Topology.IsInducing.specializes_iff, Set.Mem, Iff.symm, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂

Tactic:
simp only [Specializes, nhds_prod_eq, prod_le_prod]

Premises used: Specializes, Filter.prod_le_prod, nhds_prod_eq
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x₁ x₂ : X
y₁ y₂ : Y
hx : x₁ ⤳ x₂
hy : y₁ ⤳ y₂
⊢ (x₁, y₁) ⤳ (x₂, y₂)

Tactic:
specializes_prod.2 ⟨hx, hy⟩

Premises used: Iff.mpr, specializes_prod, And.intro
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a b : X × Y
h : a ⤳ b
⊢ a.1 ⤳ b.1

Tactic:
(specializes_prod.1 h).1

Premises used: specializes_prod, And.left, Iff.mp
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
a b : X × Y
h : a ⤳ b
⊢ a.2 ⤳ b.2

Tactic:
(specializes_prod.1 h).2

Premises used: specializes_prod, And.right, Iff.mp
-- Module: Mathlib.Topology.Inseparable
Goal:
ι : Type u_5
A : ι → Type u_6
inst : (i : ι) → TopologicalSpace (A i)
f g : (i : ι) → A i
⊢ f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i

Tactic:
simp only [Specializes, nhds_pi, pi_le_pi]

Premises used: Filter.pi_le_pi, Specializes, nhds_pi
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
rw : (¬∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S
⊢ ¬x ⤳ y ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S

Tactic:
rw [specializes_iff_forall_open]

Premises used: specializes_iff_forall_open
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
push : (∃ (s : Set X), IsOpen[inst] s ∧ y ∈ s ∧ x ∉ s) ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S
⊢ (¬∀ (s : Set X), IsOpen[inst] s → y ∈ s → x ∈ s) ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (∃ (s : Set X), IsOpen[inst] s ∧ y ∈ s ∧ x ∉ s) ↔ ∃ (S : Set X), IsOpen[inst] S ∧ y ∈ S ∧ x ∉ S

Tactic:
rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
rw : (¬∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s) ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S
⊢ ¬x ⤳ y ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S

Tactic:
rw [specializes_iff_forall_closed]

Premises used: specializes_iff_forall_closed
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
push : (∃ (s : Set X), IsClosed[inst] s ∧ x ∈ s ∧ y ∉ s) ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S
⊢ (¬∀ (s : Set X), IsClosed[inst] s → x ∈ s → y ∈ s) ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (∃ (s : Set X), IsClosed[inst] s ∧ x ∈ s ∧ y ∉ s) ↔ ∃ (S : Set X), IsClosed[inst] S ∧ x ∈ S ∧ y ∉ S

Tactic:
rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
⊢ ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U

Tactic:
have : ∀ U, IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U
rw : ∀ (s_1 : Set Y), IsOpen[inst_1] s_1 → IsOpen[inst] (s.piecewise (β := fun (a : X) ↦ Y) f g ⁻¹' s_1)
⊢ Continuous[inst, inst_1] (s.piecewise (β := fun (a : X) ↦ Y) f g)

Tactic:
rw [continuous_def]

Premises used: continuous_def
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst_1] U
rw : IsOpen[inst] (f ⁻¹' U ∩ s ∪ g ⁻¹' U)
⊢ IsOpen[inst] (s.piecewise (β := fun (a : X) ↦ Y) f g ⁻¹' U)

Tactic:
rw [piecewise_preimage, ite_eq_of_subset_right _ (this U hU)]

Premises used: Set.ite_eq_of_subset_right, Set.piecewise_preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst_1] U
⊢ IsOpen[inst] (f ⁻¹' U ∩ s ∪ g ⁻¹' U)

Tactic:
hU.preimage hf |>.inter hs |>.union (hU.preimage hg)

Premises used: IsOpen.union, IsOpen.inter, IsOpen.preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsOpen[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst_1] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst_1] U
⊢ IsOpen[inst] (f ⁻¹' U ∩ s ∪ g ⁻¹' U)

Tactic:
exact hU.preimage hf |>.inter hs |>.union (hU.preimage hg)

Premises used: IsOpen.union, IsOpen.inter, IsOpen.preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f g : X → Y
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : IsClosed[inst] s
hf : Continuous[inst, inst_1] f
hg : Continuous[inst, inst_1] g
hspec : ∀ (x : X), g x ⤳ f x
⊢ Continuous[inst, inst_1] (s.piecewise (β := fun (a : X) ↦ Y) f g)

Tactic:
simpa only [piecewise_compl] using hs.isOpen_compl.continuous_piecewise_of_specializes hg hf hspec

Premises used: IsOpen.continuous_piecewise_of_specializes, IsClosed.isOpen_compl, Set.piecewise_compl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
f : Filter X
h : x ⤳ y
hx : ClusterPt x f
⊢ ClusterPt y f

Tactic:
Filter.NeBot.mono hx <| inf_le_inf_right _ h

Premises used: Filter.NeBot.mono, inf_le_inf_right, ClusterPt
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
_ : ∀ [f.NeBot], f ≤ 𝓟 t → ∃ x ∈ t, ClusterPt x f
⊢ ∀ [f.NeBot], f ≤ 𝓟 t → ∃ x ∈ t, ClusterPt x f

Tactic:
_
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst_1 : f.NeBot
hf : f ≤ 𝓟 t
obtain : ∀ (x : X) (hxs : x ∈ s) (hxf : ClusterPt x f), ∃ x ∈ t, ClusterPt x f
⊢ ∃ x ∈ t, ClusterPt x f

Tactic:
obtain ⟨x, hxs, hxf⟩ := hs <| hf.trans <| Filter.monotone_principal hts

Premises used: LE.le.trans, Filter.monotone_principal
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst_1 : f.NeBot
hf : f ≤ 𝓟 t
x : X
hxs : x ∈ s
hxf : ClusterPt x f
obtain : ∀ (y : X) (hyt : y ∈ t) (hxy : x ⤳ y), ∃ x ∈ t, ClusterPt x f
⊢ ∃ x ∈ t, ClusterPt x f

Tactic:
obtain ⟨y, hyt, hxy⟩ := h x hxs
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst_1 : f.NeBot
hf : f ≤ 𝓟 t
x : X
hxs : x ∈ s
hxf : ClusterPt x f
y : X
hyt : y ∈ t
hxy : x ⤳ y
⊢ ∃ x ∈ t, ClusterPt x f

Tactic:
⟨y, hyt, hxy.clusterPt hxf⟩

Premises used: Specializes.clusterPt, And.intro, Exists.intro
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
f : Filter X
inst_1 : f.NeBot
hf : f ≤ 𝓟 t
x : X
hxs : x ∈ s
hxf : ClusterPt x f
y : X
hyt : y ∈ t
hxy : x ⤳ y
⊢ ∃ x ∈ t, ClusterPt x f

Tactic:
exact ⟨y, hyt, hxy.clusterPt hxf⟩
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ Monotone f

Tactic:
fun _ _ h => h.map hf

Premises used: Monotone, Specializes.map
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ closure[inst] {x} = Iic x

Tactic:
Set.ext fun _ ↦ specializes_iff_mem_closure.symm

Premises used: Set.ext, specializes_iff_mem_closure, Iff.symm
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : (i : ι) → TopologicalSpace (A i)
x y z : X
s_1 : Set X
f g : X → Y
s : Set X
⊢ StableUnderSpecialization s ↔ IsLowerSet s

Tactic:
Iff.rfl

Premises used: StableUnderSpecialization, Iff.rfl, IsLowerSet
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
ι : Type u_5
A : ι → Type u_6
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : (i : ι) → TopologicalSpace (A i)
x y z : X
s_1 : Set X
f g : X → Y
s : Set X
⊢ StableUnderGeneralization s ↔ IsUpperSet s

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsUpperSet, StableUnderGeneralization
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ StableUnderSpecialization s

Tactic:
fun _ _ e ↦ e.mem_closed hs

Premises used: StableUnderSpecialization, Specializes.mem_closed
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
⊢ StableUnderGeneralization s

Tactic:
fun _ _ e ↦ e.mem_open hs

Premises used: Specializes.mem_open, StableUnderGeneralization
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization sᶜ ↔ StableUnderGeneralization s

Tactic:
isLowerSet_compl

Premises used: StableUnderSpecialization, IsUpperSet, StableUnderGeneralization, isLowerSet_compl, IsLowerSet
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization sᶜ ↔ StableUnderSpecialization s

Tactic:
isUpperSet_compl

Premises used: StableUnderSpecialization, IsUpperSet, StableUnderGeneralization, IsLowerSet, isUpperSet_compl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ StableUnderSpecialization.{u_1} (X := X) univ

Tactic:
isLowerSet_univ

Premises used: StableUnderSpecialization, isLowerSet_univ, IsLowerSet
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ StableUnderSpecialization.{u_1} (X := X) ∅

Tactic:
isLowerSet_empty

Premises used: StableUnderSpecialization, IsLowerSet, isLowerSet_empty
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ StableUnderGeneralization.{u_1} (X := X) univ

Tactic:
isUpperSet_univ

Premises used: IsUpperSet, StableUnderGeneralization, isUpperSet_univ
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ StableUnderGeneralization.{u_1} (X := X) ∅

Tactic:
isUpperSet_empty

Premises used: IsUpperSet, StableUnderGeneralization, isUpperSet_empty
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
H : ∀ s ∈ S, StableUnderSpecialization s
⊢ StableUnderSpecialization (⋃₀ S)

Tactic:
isLowerSet_sUnion H

Premises used: StableUnderSpecialization, IsLowerSet, isLowerSet_sUnion
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
H : ∀ s ∈ S, StableUnderSpecialization s
⊢ StableUnderSpecialization (⋂₀ S)

Tactic:
isLowerSet_sInter H

Premises used: StableUnderSpecialization, isLowerSet_sInter, IsLowerSet
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
H : ∀ s ∈ S, StableUnderGeneralization s
⊢ StableUnderGeneralization (⋃₀ S)

Tactic:
isUpperSet_sUnion H

Premises used: IsUpperSet, StableUnderGeneralization, isUpperSet_sUnion
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
H : ∀ s ∈ S, StableUnderGeneralization s
⊢ StableUnderGeneralization (⋂₀ S)

Tactic:
isUpperSet_sInter H

Premises used: IsUpperSet, StableUnderGeneralization, isUpperSet_sInter
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Sort u_7
S : ι → Set X
H : ∀ (i : ι), StableUnderSpecialization (S i)
⊢ StableUnderSpecialization.{u_1} (X := X) (⋃ (i : ι), S i)

Tactic:
isLowerSet_iUnion H

Premises used: StableUnderSpecialization, isLowerSet_iUnion, IsLowerSet
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Sort u_7
S : ι → Set X
H : ∀ (i : ι), StableUnderSpecialization (S i)
⊢ StableUnderSpecialization.{u_1} (X := X) (⋂ (i : ι), S i)

Tactic:
isLowerSet_iInter H

Premises used: StableUnderSpecialization, IsLowerSet, isLowerSet_iInter
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Sort u_7
S : ι → Set X
H : ∀ (i : ι), StableUnderGeneralization (S i)
⊢ StableUnderGeneralization.{u_1} (X := X) (⋃ (i : ι), S i)

Tactic:
isUpperSet_iUnion H

Premises used: IsUpperSet, StableUnderGeneralization, isUpperSet_iUnion
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Sort u_7
S : ι → Set X
H : ∀ (i : ι), StableUnderGeneralization (S i)
⊢ StableUnderGeneralization.{u_1} (X := X) (⋂ (i : ι), S i)

Tactic:
isUpperSet_iInter H

Premises used: IsUpperSet, StableUnderGeneralization, isUpperSet_iInter
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ ⋃ x ∈ s, closure[inst] {x} = s ↔ IsLowerSet s

Tactic:
simp only [closure_singleton_eq_Iic, ← lowerClosure_eq, coe_lowerClosure]

Premises used: coe_lowerClosure, lowerClosure_eq, closure_singleton_eq_Iic
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization s ↔ ⋃ x ∈ s, closure[inst] {x} = s

Tactic:
Union_closure_singleton_eq_iff.symm

Premises used: Union_closure_singleton_eq_iff, Iff.symm
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = s

Tactic:
⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩

Premises used: StableUnderSpecialization, Eq.rec, _private.0.stableUnderSpecialization_iff_exists_sUnion_eq.match_1, stableUnderSpecialization_sUnion, closure, IsClosed.stableUnderSpecialization, And.intro, Iff.intro, Exists.intro, Set.image, Singleton.singleton
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine_1 :
  ∀ (H : StableUnderSpecialization s) (s_1 : Set X),
    Membership.mem (γ := Set (Set X)) ((fun (x : X) ↦ closure[inst] {x}) '' s) s_1 → IsClosed[inst] s_1
refine_2 : ∀ (H : StableUnderSpecialization s), ⋃₀ ((fun (x : X) ↦ closure[inst] {x}) '' s) = s
⊢ StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = s

Tactic:
refine ⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
w : X
left : w ∈ s
⊢ IsClosed[inst] ((fun (x : X) ↦ (closure[inst] {x} : Set X)) w)

Tactic:
isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
w : X
left : w ∈ s
⊢ IsClosed[inst] ((fun (x : X) ↦ (closure[inst] {x} : Set X)) w)

Tactic:
exact isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
rw : ⋃ x ∈ s, closure[inst] {x}
| s

Tactic:
rw [← H.Union_eq]

Premises used: StableUnderSpecialization.Union_eq
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
refine_2 : Eq (α := Set X) (⋃₀ ((fun (x : X) ↦ closure[inst] {x}) '' s)) (⋃ x ∈ s, closure[inst] {x})
⊢ ⋃₀ ((fun (x : X) ↦ closure[inst] {x}) '' s) = s

Tactic:
conv_rhs => rw [← H.Union_eq]

Premises used: StableUnderSpecialization.Union_eq
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
⊢ Eq (α := Set X) (⋃₀ ((fun (x : X) ↦ closure[inst] {x}) '' s)) (⋃ x ∈ s, closure[inst] {x})

Tactic:
simp