awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s

Tactic:
⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩

Premises used: stableUnderGeneralization_sInter, Eq.rec, StableUnderGeneralization, Iff.intro, _private.0.stableUnderGeneralization_iff_exists_sInter_eq.match_1, IsOpen.stableUnderGeneralization
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
refine : StableUnderGeneralization s → ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s
⊢ StableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s

Tactic:
refine ⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw :
  (∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = sᶜ) →
    ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s
⊢ StableUnderGeneralization s → ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s

Tactic:
rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]

Premises used: stableUnderSpecialization_iff_exists_sUnion_eq, stableUnderSpecialization_compl_iff
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = sᶜ) →
    ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s

Tactic:
fun ⟨S, h₁, h₂⟩ ↦ ⟨(·ᶜ) '' S, fun s ⟨t, ht, e⟩ ↦ e ▸ (h₁ t ht).isOpen_compl,
    compl_injective ((sUnion_eq_compl_sInter_compl S).symm.trans h₂)⟩

Premises used: _private.0.stableUnderGeneralization_iff_exists_sInter_eq.match_3, IsClosed.isOpen_compl, Compl.compl, Exists, Eq.rec, compl_injective, And, Set.sUnion_eq_compl_sInter_compl, And.intro, Exists.intro, Set.image, IsOpen, _private.0.stableUnderGeneralization_iff_exists_sInter_eq.match_2, Eq.symm, Eq, Set.sInter, Eq.trans
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ (∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed[inst] s) ∧ ⋃₀ S = sᶜ) →
    ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen[inst] s) ∧ ⋂₀ S = s

Tactic:
exact fun ⟨S, h₁, h₂⟩ ↦ ⟨(·ᶜ) '' S, fun s ⟨t, ht, e⟩ ↦ e ▸ (h₁ t ht).isOpen_compl,
    compl_injective ((sUnion_eq_compl_sInter_compl S).symm.trans h₂)⟩
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : StableUnderSpecialization s
hf : Continuous[inst, inst_1] f
⊢ StableUnderSpecialization (f ⁻¹' s)

Tactic:
IsLowerSet.preimage hs hf.specialization_monotone

Premises used: StableUnderSpecialization, IsLowerSet.preimage, IsLowerSet, Continuous.specialization_monotone
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
s : Set Y
hs : StableUnderGeneralization s
hf : Continuous[inst, inst_1] f
⊢ StableUnderGeneralization (f ⁻¹' s)

Tactic:
IsUpperSet.preimage hs hf.specialization_monotone

Premises used: IsUpperSet, IsUpperSet.preimage, StableUnderGeneralization, Continuous.specialization_monotone
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
simp :
  (∀ ⦃a : X⦄ ⦃b : Y⦄,
      Membership.mem (γ := Set Y) (closure[inst_1] {f a}) b →
        ∃ (a' : X), Membership.mem (γ := Set X) (closure[inst] {a}) a' ∧ f a' = b) ↔
    ∀ (x : X), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}
⊢ SpecializingMap f ↔ ∀ (x : X), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}

Tactic:
simp only [SpecializingMap, Relation.Fibration, flip, specializes_iff_mem_closure]

Premises used: SpecializingMap, specializes_iff_mem_closure, flip, Relation.Fibration
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ (∀ ⦃a : X⦄ ⦃b : Y⦄,
      Membership.mem (γ := Set Y) (closure[inst_1] {f a}) b →
        ∃ (a' : X), Membership.mem (γ := Set X) (closure[inst] {a}) a' ∧ f a' = b) ↔
    ∀ (x : X), closure[inst_1] {f x} ⊆ f '' closure[inst] {x}

Tactic:
rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : SpecializingMap f
s : Set X
hs : StableUnderSpecialization s
⊢ StableUnderSpecialization (f '' s)

Tactic:
IsLowerSet.image_fibration hf hs

Premises used: StableUnderSpecialization, IsLowerSet, IsLowerSet.image_fibration
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure[inst] {x})

Tactic:
simpa only [closure_singleton_eq_Iic] using Relation.fibration_iff_isLowerSet_image_Iic

Premises used: Relation.fibration_iff_isLowerSet_image_Iic, closure_singleton_eq_Iic
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)

Tactic:
Relation.fibration_iff_isLowerSet_image

Premises used: StableUnderSpecialization, Relation.fibration_iff_isLowerSet_image, SpecializingMap, IsLowerSet
-- 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
⊢ SpecializingMap f ↔ ∀ (x : X), f '' closure[inst] {x} = closure[inst_1] {f x}

Tactic:
simpa only [closure_singleton_eq_Iic] using
    Relation.fibration_iff_image_Iic hf.specialization_monotone

Premises used: Relation.fibration_iff_image_Iic, Continuous.specialization_monotone, closure_singleton_eq_Iic
-- 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
⊢ SpecializingMap f ↔ ∀ (x : X), IsClosed[inst_1] (f '' closure[inst] {x})

Tactic:
⟨fun h x ↦ ?_, fun h ↦ specializingMap_iff_stableUnderSpecialization_image_singleton.mpr
    (fun x ↦ (h x).stableUnderSpecialization)⟩

Premises used: Iff.mpr, IsClosed.stableUnderSpecialization, Iff.intro, specializingMap_iff_stableUnderSpecialization_image_singleton
-- 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
refine : ∀ (h : SpecializingMap f) (x : X), IsClosed[inst_1] (f '' closure[inst] {x})
⊢ SpecializingMap f ↔ ∀ (x : X), IsClosed[inst_1] (f '' closure[inst] {x})

Tactic:
refine ⟨fun h x ↦ ?_, fun h ↦ specializingMap_iff_stableUnderSpecialization_image_singleton.mpr
    (fun x ↦ (h x).stableUnderSpecialization)⟩
-- 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
h : SpecializingMap f
x : X
rw : IsClosed[inst_1] (closure[inst_1] {f x})
⊢ IsClosed[inst_1] (f '' closure[inst] {x})

Tactic:
rw [(specializingMap_iff_closure_singleton hf).mp h x]

Premises used: Iff.mp, specializingMap_iff_closure_singleton
-- 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
h : SpecializingMap f
x : X
⊢ IsClosed[inst_1] (closure[inst_1] {f x})

Tactic:
isClosed_closure

Premises used: isClosed_closure
-- 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
h : SpecializingMap f
x : X
⊢ IsClosed[inst_1] (closure[inst_1] {f x})

Tactic:
exact isClosed_closure

Premises used: isClosed_closure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : SpecializingMap f
hg : SpecializingMap g
simp :
  ∀ (hf : ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s))
    (hg : ∀ (s : Set Y), StableUnderSpecialization s → StableUnderSpecialization (g '' s)) (s : Set X),
    StableUnderSpecialization s → StableUnderSpecialization (g '' f '' s)
⊢ SpecializingMap (g ∘ f)

Tactic:
simp only [specializingMap_iff_stableUnderSpecialization_image, Set.image_comp] at *

Premises used: specializingMap_iff_stableUnderSpecialization_image, Set.image_comp
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)
hg : ∀ (s : Set Y), StableUnderSpecialization s → StableUnderSpecialization (g '' s)
⊢ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (g '' f '' s)

Tactic:
fun s h ↦ hg _ (hf _ h)

Premises used: Set.image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (f '' s)
hg : ∀ (s : Set Y), StableUnderSpecialization s → StableUnderSpecialization (g '' s)
⊢ ∀ (s : Set X), StableUnderSpecialization s → StableUnderSpecialization (g '' f '' s)

Tactic:
exact fun s h ↦ hg _ (hf _ h)

Premises used: Set.image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedMap f
⊢ SpecializingMap f

Tactic:
specializingMap_iff_stableUnderSpecialization_image_singleton.mpr <|
    fun _ ↦ (hf _ isClosed_closure).stableUnderSpecialization

Premises used: Iff.mpr, closure, IsClosed.stableUnderSpecialization, specializingMap_iff_stableUnderSpecialization_image_singleton, Singleton.singleton, isClosed_closure
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x : X
y : Y
e : flip (fun (x1 x2 : Y) ↦ x1 ⤳ x2) y (f x)
obtain :
  ∀ (y : X) (e : flip (fun (x1 x2 : Y) ↦ x1 ⤳ x2) (f y) (f x)),
    ∃ (a' : X), flip (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y
⊢ ∃ (a' : X), flip (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x y : X
e : flip (fun (x1 x2 : Y) ↦ x1 ⤳ x2) (f y) (f x)
⊢ ∃ (a' : X), flip (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
⟨_, hf.specializes_iff.mp e, rfl⟩

Premises used: Topology.IsInducing.specializes_iff, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
x y : X
e : flip (fun (x1 x2 : Y) ↦ x1 ⤳ x2) (f y) (f x)
⊢ ∃ (a' : X), flip (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
exact ⟨_, hf.specializes_iff.mp e, rfl⟩
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x : X
y : Y
e : y ⤳ f x
obtain : ∀ (y : X) (e : f y ⤳ f x), ∃ (a' : X), (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y
⊢ ∃ (a' : X), (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = y

Tactic:
obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x y : X
e : f y ⤳ f x
⊢ ∃ (a' : X), (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
⟨_, hf.specializes_iff.mp e, rfl⟩

Premises used: Topology.IsInducing.specializes_iff, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
x y : X
e : f y ⤳ f x
⊢ ∃ (a' : X), (fun (x1 x2 : X) ↦ x1 ⤳ x2) a' x ∧ f a' = f y

Tactic:
exact ⟨_, hf.specializes_iff.mp e, rfl⟩
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
⊢ GeneralizingMap f

Tactic:
hf.isInducing.generalizingMap hf.isOpen_range.stableUnderGeneralization

Premises used: Topology.IsInducing.generalizingMap, Topology.IsOpenEmbedding.isOpen_range, Topology.IsOpenEmbedding.isInducing, IsOpen.stableUnderGeneralization
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : SpecializingMap f
⊢ StableUnderSpecialization (range f)

Tactic:
@image_univ _ _ f ▸ stableUnderSpecialization_univ.image h

Premises used: Set.image_univ, Eq.rec, StableUnderSpecialization.image, stableUnderSpecialization_univ
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : GeneralizingMap f
s : Set X
hs : StableUnderGeneralization s
⊢ StableUnderGeneralization (f '' s)

Tactic:
IsUpperSet.image_fibration hf hs

Premises used: IsUpperSet, IsUpperSet.image_fibration, StableUnderGeneralization
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ GeneralizingMap f ↔ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)

Tactic:
Relation.fibration_iff_isUpperSet_image

Premises used: GeneralizingMap, IsUpperSet, Relation.fibration_iff_isUpperSet_image, StableUnderGeneralization
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
h : GeneralizingMap f
⊢ StableUnderGeneralization (range f)

Tactic:
@image_univ _ _ f ▸ stableUnderGeneralization_univ.image h

Premises used: Set.image_univ, Eq.rec, stableUnderGeneralization_univ, StableUnderGeneralization.image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : GeneralizingMap f
hg : GeneralizingMap g
simp :
  ∀ (hf : ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s))
    (hg : ∀ (s : Set Y), StableUnderGeneralization s → StableUnderGeneralization (g '' s)) (s : Set X),
    StableUnderGeneralization s → StableUnderGeneralization (g '' f '' s)
⊢ GeneralizingMap (g ∘ f)

Tactic:
simp only [GeneralizingMap_iff_stableUnderGeneralization_image, Set.image_comp] at *

Premises used: Set.image_comp, GeneralizingMap_iff_stableUnderGeneralization_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)
hg : ∀ (s : Set Y), StableUnderGeneralization s → StableUnderGeneralization (g '' s)
⊢ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (g '' f '' s)

Tactic:
fun s h ↦ hg _ (hf _ h)

Premises used: Set.image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (f '' s)
hg : ∀ (s : Set Y), StableUnderGeneralization s → StableUnderGeneralization (g '' s)
⊢ ∀ (s : Set X), StableUnderGeneralization s → StableUnderGeneralization (g '' f '' s)

Tactic:
exact fun s h ↦ hg _ (hf _ h)

Premises used: Set.image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ 𝓝 x = 𝓝 y

Tactic:
Iff.rfl

Premises used: Iff.rfl, Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ x ⤳ y ∧ y ⤳ x

Tactic:
le_antisymm_iff

Premises used: Specializes, le_antisymm_iff, Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ~ᵢ y
⊢ x ⤳ y

Tactic:
h.le

Premises used: Specializes, Eq.le
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ~ᵢ y
⊢ y ⤳ x

Tactic:
h.ge

Premises used: Eq.ge, Specializes
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h₁ : x ⤳ y
h₂ : y ⤳ x
⊢ x ~ᵢ y

Tactic:
le_antisymm h₁ h₂

Premises used: le_antisymm, Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsOpen[inst] s → (x ∈ s ↔ y ∈ s)

Tactic:
simp only [inseparable_iff_specializes_and, specializes_iff_forall_open, ← forall_and, ← iff_def,
    Iff.comm]

Premises used: inseparable_iff_specializes_and, iff_def, Iff.comm, specializes_iff_forall_open, forall_and
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ ¬(x ~ᵢ y) ↔ ∃ (s : Set X), IsOpen[inst] s ∧ Xor (x ∈ s) (y ∈ s)

Tactic:
simp [inseparable_iff_forall_isOpen, ← xor_iff_not_iff]

Premises used: xor_iff_not_iff, inseparable_iff_forall_isOpen
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsClosed[inst] s → (x ∈ s ↔ y ∈ s)

Tactic:
simp only [inseparable_iff_specializes_and, specializes_iff_forall_closed, ← forall_and, ←
    iff_def]

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

Tactic:
simp only [specializes_iff_mem_closure, and_comm]

Premises used: specializes_iff_mem_closure, and_comm
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ Eq (α := Set X) (closure[inst] {x}) (closure[inst] {y})

Tactic:
simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset, ← subset_antisymm_iff,
    eq_comm]

Premises used: inseparable_iff_specializes_and, eq_comm, subset_antisymm_iff, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
s : Set X
hx : x ∈ s
hy : y ∈ s
h : 𝓝[s] x = 𝓝[s] y
⊢ x ~ᵢ y

Tactic:
(specializes_of_nhdsWithin h.le hx).antisymm (specializes_of_nhdsWithin h.ge hy)

Premises used: Eq.ge, Eq.le, Specializes.antisymm, specializes_of_nhdsWithin
-- 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 [inseparable_iff_specializes_and, hf.specializes_iff]

Premises used: Topology.IsInducing.specializes_iff, inseparable_iff_specializes_and
-- 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.inseparable_iff.symm

Premises used: Set.Mem, Iff.symm, Topology.IsInducing.subtypeVal, Topology.IsInducing.inseparable_iff
-- 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 [Inseparable, nhds_prod_eq, Filter.prod_inj]

Premises used: Filter.prod_inj, nhds_prod_eq, Inseparable
-- 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:
inseparable_prod.2 ⟨hx, hy⟩

Premises used: Iff.mpr, And.intro, inseparable_prod
-- 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 [Inseparable, nhds_pi, funext_iff, pi_inj]

Premises used: Filter.pi_inj, funext_iff, nhds_pi, Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ x ~ᵢ x

Tactic:
Eq.refl (𝓝 x)

Premises used: nhds, Eq.refl, Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ x ~ᵢ x

Tactic:
refl x

Premises used: Inseparable.refl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
e : x = y
⊢ x ~ᵢ y

Tactic:
e ▸ refl x

Premises used: Eq.rec, Inseparable.refl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ~ᵢ y
⊢ y ~ᵢ x

Tactic:
h.symm

Premises used: Eq.symm, Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y z : X
h₁ : x ~ᵢ y
h₂ : y ~ᵢ z
⊢ x ~ᵢ z

Tactic:
h₁.trans h₂

Premises used: Eq.trans, Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
h : x ~ᵢ y
⊢ 𝓝 x = 𝓝 y

Tactic:
h

Premises used: Inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
s : Set X
h : x ~ᵢ y
hs : IsOpen[inst] s
⊢ x ∈ s ↔ y ∈ s

Tactic:
inseparable_iff_forall_isOpen.1 h s hs

Premises used: inseparable_iff_forall_isOpen, Iff.mp
-- 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
⊢ x ∈ s ↔ y ∈ s

Tactic:
inseparable_iff_forall_isClosed.1 h s hs

Premises used: inseparable_iff_forall_isClosed, Iff.mp
-- 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 t : Set X
h : x ~ᵢ y
hfx : ContinuousWithinAt f s x
hfy : ContinuousWithinAt f t y
hx : x ∈ t
hy : y ∈ s
⊢ f x ~ᵢ f y

Tactic:
(h.specializes.map_of_continuousWithinAt hfy hx).antisymm
    (h.specializes'.map_of_continuousWithinAt hfx hy)

Premises used: Inseparable.specializes', Specializes.antisymm, Specializes.map_of_continuousWithinAt, Inseparable.specializes
-- 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 hx) (hf.continuousWithinAt hy) hx hy

Premises used: Inseparable.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
hx : ContinuousAt f x
hy : ContinuousAt f y
⊢ f x ~ᵢ f y

Tactic:
h.map_of_continuousWithinAt hx.continuousWithinAt hy.continuousWithinAt (mem_univ x) (mem_univ y)

Premises used: ContinuousAt.continuousWithinAt, Inseparable.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 hf.continuousAt

Premises used: Inseparable.map_of_continuousAt, Continuous.continuousAt
-- 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_iff hs).1 hx

Premises used: Inseparable.mem_closed_iff, Iff.mp, Not