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
hs : IsOpen[inst] s
hx : x ∈ s
hy : y ∉ s
⊢ ¬(x ~ᵢ y)

Tactic:
fun h =>
  hy <| (h.mem_open_iff hs).1 hx

Premises used: Iff.mp, Inseparable.mem_open_iff, Not
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsQuotientMap.{u_1, u_1} (X := X) (Y := SeparationQuotient X) mk

Tactic:
isQuotientMap_quot_mk

Premises used: Quotient, Quotient.mk', SeparationQuotient, SeparationQuotient.mk, isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Continuous[inst, _] mk

Tactic:
continuous_quot_mk

Premises used: Quotient, continuous_quot_mk, Quotient.mk', SeparationQuotient, SeparationQuotient.mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x y : X
⊢ Eq (α := SeparationQuotient X) (mk x) (mk y) ↔ (x ~ᵢ y)

Tactic:
Quotient.eq''

Premises used: Quotient.eq'', SeparationQuotient, SeparationQuotient.mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
P : SeparationQuotient X → Prop
⊢ (∀ (x : SeparationQuotient X), P x) ↔ ∀ (x : X), P (mk x)

Tactic:
Quotient.forall

Premises used: Quotient.forall, SeparationQuotient, SeparationQuotient.mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
P : SeparationQuotient X → Prop
⊢ (∃ (x : SeparationQuotient X), P x) ↔ ∃ (x : X), P (mk x)

Tactic:
Quotient.exists

Premises used: SeparationQuotient, SeparationQuotient.mk, Quotient.exists
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := X) (β := SeparationQuotient X) mk

Tactic:
Quot.mk_surjective

Premises used: Quotient, SeparationQuotient, SeparationQuotient.mk, Quot.mk_surjective
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq.{u_1 + 1} (α := Set (SeparationQuotient X)) (range mk) univ

Tactic:
surjective_mk.range_eq

Premises used: Function.Surjective.range_eq, SeparationQuotient.surjective_mk
-- 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 : Set X
f g : X → Y
t : Set (SeparationQuotient X)
inst_4 : Nonempty X
⊢ Nonempty.{u_1 + 1} (SeparationQuotient X)

Tactic:
Nonempty.map mk ‹_›

Premises used: SeparationQuotient.mk, Nonempty.map
-- 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 : Set X
f g : X → Y
t : Set (SeparationQuotient X)
inst_4 : Subsingleton X
⊢ Subsingleton.{u_1 + 1} (SeparationQuotient X)

Tactic:
surjective_mk.subsingleton

Premises used: Function.Surjective.subsingleton, SeparationQuotient.surjective_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
α : Type u_4
inst : TopologicalSpace α
⊢ inseparableSetoid α = ⊤ ↔ IndiscreteTopology α

Tactic:
Setoid.eq_top_iff.trans TopologicalSpace.indiscrete_iff_forall_inseparable.symm

Premises used: Setoid.eq_top_iff, Iff.trans, TopologicalSpace.indiscrete_iff_forall_inseparable, Iff.symm
-- Module: Mathlib.Topology.Inseparable
Goal:
α : Type u_4
inst : TopologicalSpace α
⊢ Subsingleton.{u_4 + 1} (SeparationQuotient α) ↔ IndiscreteTopology α

Tactic:
Quotient.subsingleton_iff.trans inseparableSetoid_eq_top_iff

Premises used: Quotient.subsingleton_iff, SeparationQuotient.inseparableSetoid_eq_top_iff, SeparationQuotient, Iff.trans
-- 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 : Set X
f g : X → Y
t : Set (SeparationQuotient X)
inst_4 : TopologicalSpace α
inst_5 : IndiscreteTopology α
⊢ Subsingleton.{u_4 + 1} (SeparationQuotient α)

Tactic:
subsingleton_iff.2 ‹_›

Premises used: Iff.mpr, SeparationQuotient.subsingleton_iff
-- 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 : Set X
f g : X → Y
t : Set (SeparationQuotient X)
inst_4 : TopologicalSpace α
inst_5 : IndiscreteTopology α
p : α → Prop
⊢ IndiscreteTopology.{u_4} (Subtype p)

Tactic:
simp [TopologicalSpace.indiscrete_iff_forall_inseparable, subtype_inseparable_iff]

Premises used: subtype_inseparable_iff, TopologicalSpace.indiscrete_iff_forall_inseparable
-- Module: Mathlib.Topology.Inseparable
Goal:
α : Type u_4
inst : TopologicalSpace α
⊢ Nontrivial.{u_4} (SeparationQuotient α) ↔ NontrivialTopology α

Tactic:
simpa [not_subsingleton_iff_nontrivial] using subsingleton_iff.not

Premises used: Iff.not, not_subsingleton_iff_nontrivial, SeparationQuotient.subsingleton_iff
-- 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 : Set X
f g : X → Y
t : Set (SeparationQuotient X)
inst_4 : TopologicalSpace α
inst_5 : NontrivialTopology α
⊢ Nontrivial.{u_4} (SeparationQuotient α)

Tactic:
nontrivial_iff.2 ‹_›

Premises used: Iff.mpr, SeparationQuotient.nontrivial_iff
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : One X
⊢ Eq.{u_1 + 1} (α := SeparationQuotient X) (mk 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
⊢ preimage (β := SeparationQuotient X) mk (mk '' s) = s

Tactic:
Subset.antisymm ?_ (subset_preimage_image _ _)

Premises used: Set.Subset.antisymm, Set.subset_preimage_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
refine : preimage (β := SeparationQuotient X) mk (mk '' s) ⊆ s
⊢ preimage (β := SeparationQuotient X) mk (mk '' s) = s

Tactic:
refine Subset.antisymm ?_ (subset_preimage_image _ _)

Premises used: Set.Subset.antisymm, Set.subset_preimage_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
x y : X
hys : y ∈ s
hxy : Eq (α := SeparationQuotient X) (mk y) (mk x)
⊢ x ∈ s

Tactic:
((mk_eq_mk.1 hxy).mem_open_iff hs).1 hys

Premises used: SeparationQuotient.mk_eq_mk, Iff.mp, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
x y : X
hys : y ∈ s
hxy : Eq (α := SeparationQuotient X) (mk y) (mk x)
⊢ x ∈ s

Tactic:
exact ((mk_eq_mk.1 hxy).mem_open_iff hs).1 hys

Premises used: SeparationQuotient.mk_eq_mk, Iff.mp, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs rwa rwa₁ rwa₂ rwa₃ : IsOpen[inst] s
⊢ IsOpen[inst] (preimage (β := SeparationQuotient X) mk (mk '' s))

Tactic:
rwa [preimage_image_mk_open hs]

Premises used: SeparationQuotient.preimage_image_mk_open
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsOpenQuotientMap.{u_1, u_1} (X := X) (Y := SeparationQuotient X) mk

Tactic:
⟨surjective_mk, continuous_mk, isOpenMap_mk⟩

Premises used: SeparationQuotient.continuous_mk, IsOpenQuotientMap.mk, SeparationQuotient.isOpenMap_mk, SeparationQuotient.surjective_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
⊢ preimage (β := SeparationQuotient X) mk (mk '' s) = s

Tactic:
Subset.antisymm ?_ (subset_preimage_image _ _)

Premises used: Set.Subset.antisymm, Set.subset_preimage_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
refine : preimage (β := SeparationQuotient X) mk (mk '' s) ⊆ s
⊢ preimage (β := SeparationQuotient X) mk (mk '' s) = s

Tactic:
refine Subset.antisymm ?_ (subset_preimage_image _ _)

Premises used: Set.Subset.antisymm, Set.subset_preimage_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
x y : X
hys : y ∈ s
hxy : Eq (α := SeparationQuotient X) (mk y) (mk x)
⊢ x ∈ s

Tactic:
((mk_eq_mk.1 hxy).mem_closed_iff hs).1 hys

Premises used: SeparationQuotient.mk_eq_mk, Inseparable.mem_closed_iff, Iff.mp
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsClosed[inst] s
x y : X
hys : y ∈ s
hxy : Eq (α := SeparationQuotient X) (mk y) (mk x)
⊢ x ∈ s

Tactic:
exact ((mk_eq_mk.1 hxy).mem_closed_iff hs).1 hys

Premises used: SeparationQuotient.mk_eq_mk, Inseparable.mem_closed_iff, Iff.mp
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsInducing.{u_1, u_1} (X := X) (Y := SeparationQuotient X) mk

Tactic:
⟨le_antisymm (continuous_iff_le_induced.1 continuous_mk) fun s hs =>
      ⟨mk '' s, isOpenMap_mk s hs, preimage_image_mk_open hs⟩⟩

Premises used: SeparationQuotient.continuous_mk, continuous_iff_le_induced, SeparationQuotient.isOpenMap_mk, le_antisymm, Topology.IsInducing.mk, And.intro, SeparationQuotient.mk, Exists.intro, Iff.mp, Set.image, SeparationQuotient.preimage_image_mk_open
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
rw : IsClosed.{u_1} (X := SeparationQuotient X) univ
⊢ IsClosed.{u_1} (X := SeparationQuotient X) (range mk)

Tactic:
rw [range_mk]

Premises used: SeparationQuotient.range_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsClosed.{u_1} (X := SeparationQuotient X) univ

Tactic:
isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ IsClosed.{u_1} (X := SeparationQuotient X) univ

Tactic:
exact isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ comap (β := SeparationQuotient X) mk (𝓝 (mk x)) = 𝓝 x

Tactic:
(isInducing_mk.nhds_eq_comap _).symm

Premises used: Topology.IsInducing.nhds_eq_comap, SeparationQuotient.isInducing_mk, Eq.symm
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ comap (β := SeparationQuotient X) mk (𝓝ˢ (mk '' s)) = 𝓝ˢ s

Tactic:
(isInducing_mk.nhdsSet_eq_comap _).symm

Premises used: SeparationQuotient.isInducing_mk, Topology.IsInducing.nhdsSet_eq_comap, Eq.symm
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
rw : Eq (α := Filter (SeparationQuotient X)) (map mk (comap (β := SeparationQuotient X) mk (𝓝 (mk x)))) (𝓝 (mk x))
rw₁ rw₂ : Eq (α := Filter (SeparationQuotient X)) (𝓝 (mk x)) (𝓝 (mk x))
⊢ Eq (α := Filter (SeparationQuotient X)) (map mk (𝓝 x)) (𝓝 (mk x))

Tactic:
rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]

Premises used: SeparationQuotient.comap_mk_nhds_mk, Filter.map_comap_of_surjective, SeparationQuotient.surjective_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
rw :
  Eq (α := Filter (SeparationQuotient X)) (map mk (comap (β := SeparationQuotient X) mk (𝓝ˢ (mk '' s)))) (𝓝ˢ (mk '' s))
rw₁ rw₂ : Eq (α := Filter (SeparationQuotient X)) (𝓝ˢ (mk '' s)) (𝓝ˢ (mk '' s))
⊢ Eq (α := Filter (SeparationQuotient X)) (map mk (𝓝ˢ s)) (𝓝ˢ (mk '' s))

Tactic:
rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]

Premises used: Filter.map_comap_of_surjective, SeparationQuotient.surjective_mk, SeparationQuotient.comap_mk_nhdsSet_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
rw : 𝓝ˢ (mk ⁻¹' t)
| comap mk (𝓝ˢ t)

Tactic:
rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]

Premises used: Set.image_preimage_eq, SeparationQuotient.surjective_mk, SeparationQuotient.comap_mk_nhdsSet_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
conv_lhs : comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
conv_lhs₁ : 𝓝ˢ (mk ⁻¹' t) = 𝓝ˢ (mk ⁻¹' t)
⊢ comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)

Tactic:
conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]

Premises used: Set.image_preimage_eq, SeparationQuotient.surjective_mk, SeparationQuotient.comap_mk_nhdsSet_image
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
⊢ mk ⁻¹' closure t = closure[inst] (mk ⁻¹' t)

Tactic:
isOpenMap_mk.preimage_closure_eq_closure_preimage continuous_mk t

Premises used: SeparationQuotient.continuous_mk, IsOpenMap.preimage_closure_eq_closure_preimage, SeparationQuotient.isOpenMap_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
⊢ mk ⁻¹' interior t = interior (mk ⁻¹' t)

Tactic:
isOpenMap_mk.preimage_interior_eq_interior_preimage continuous_mk t

Premises used: SeparationQuotient.continuous_mk, IsOpenMap.preimage_interior_eq_interior_preimage, SeparationQuotient.isOpenMap_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
t : Set (SeparationQuotient X)
⊢ mk ⁻¹' frontier t = frontier (mk ⁻¹' t)

Tactic:
isOpenMap_mk.preimage_frontier_eq_frontier_preimage continuous_mk t

Premises used: SeparationQuotient.continuous_mk, SeparationQuotient.isOpenMap_mk, IsOpenMap.preimage_frontier_eq_frontier_preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ Eq (α := Set (SeparationQuotient X)) (mk '' closure[inst] s) (closure (mk '' s))

Tactic:
(image_closure_subset_closure_image continuous_mk).antisymm <|
    isClosedMap_mk.closure_image_subset _

Premises used: IsClosedMap.closure_image_subset, SeparationQuotient.continuous_mk, HasSubset.Subset.antisymm, image_closure_subset_closure_image, SeparationQuotient.isClosedMap_mk
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
rw :
  Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 x ×ˢ 𝓝 y))
    (𝓝 (mk x, mk y))
rw₁ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (map mk (𝓝 x)) (map mk (𝓝 y)) =
    𝓝 (mk x, mk y)
rw₂ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (map mk (𝓝 y)) =
    𝓝 (mk x, mk y)
rw₃ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (𝓝 (mk y)) =
    𝓝 (mk x, mk y)
rw₄ rw₅ :
  SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (𝓝 (mk y)) =
    SProd.sprod (α := Filter (SeparationQuotient X)) (β := Filter (SeparationQuotient Y)) (𝓝 (mk x)) (𝓝 (mk y))
⊢ Eq (α := Filter (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))) (map (Prod.map mk mk) (𝓝 (x, y)))
    (𝓝 (mk x, mk y))

Tactic:
rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]

Premises used: Filter.prod_map_map_eq', nhds_prod_eq, SeparationQuotient.map_mk_nhds
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
rw : map mk (𝓝 x ⊓ 𝓟 (mk ⁻¹' s)) = 𝓝[s] mk x
rw₁ : map mk (𝓝 x ⊓ comap mk (𝓟 s)) = 𝓝[s] mk x
rw₂ : map mk (𝓝 x) ⊓ 𝓟 s = 𝓝[s] mk x
rw₃ : map mk (𝓝 x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s
rw₄ rw₅ : 𝓝 (mk x) ⊓ 𝓟 s = 𝓝 (mk x) ⊓ 𝓟 s
⊢ map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x

Tactic:
rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]

Premises used: nhdsWithin, Filter.push_pull, Filter.comap_principal, SeparationQuotient.map_mk_nhds
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ IsQuotientMap (X := X × Y) (Y := Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y)) (Prod.map mk mk)

Tactic:
(isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).isQuotientMap

Premises used: IsOpenQuotientMap.prodMap, SeparationQuotient.isOpenQuotientMap_mk, IsOpenQuotientMap.isQuotientMap
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
α : Type u_4
inst : TopologicalSpace X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
x : X
⊢ lift f hf (mk x) = f x

Tactic:
rfl

Premises used: Quotient.liftOn', SeparationQuotient.lift, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
α : Type u_4
inst : TopologicalSpace X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
⊢ lift f hf ∘ mk = f

Tactic:
rfl

Premises used: Quotient.liftOn', SeparationQuotient.lift, rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
α : Type u_4
inst : TopologicalSpace X
x : X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
l : Filter α
⊢ Tendsto (lift f hf) (𝓝 (mk x)) l ↔ Tendsto f (𝓝 x) l

Tactic:
simp only [← map_mk_nhds, tendsto_map'_iff, lift_comp_mk]

Premises used: SeparationQuotient.lift_comp_mk, Filter.tendsto_map'_iff, SeparationQuotient.map_mk_nhds
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
α : Type u_4
inst : TopologicalSpace X
x : X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
s : Set (SeparationQuotient X)
l : Filter α
⊢ Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l

Tactic:
simp only [← map_mk_nhdsWithin_preimage, tendsto_map'_iff, lift_comp_mk]

Premises used: SeparationQuotient.lift_comp_mk, Filter.tendsto_map'_iff, SeparationQuotient.map_mk_nhdsWithin_preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
⊢ ContinuousAt (lift f hf) (mk x) ↔ ContinuousAt f x

Tactic:
tendsto_lift_nhds_mk

Premises used: SeparationQuotient.tendsto_lift_nhds_mk, Quotient.liftOn', ContinuousAt, SeparationQuotient.lift
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
s : Set (SeparationQuotient X)
⊢ ContinuousWithinAt (lift f hf) s (mk x) ↔ ContinuousWithinAt f (mk ⁻¹' s) x

Tactic:
tendsto_lift_nhdsWithin_mk

Premises used: ContinuousWithinAt, Quotient.liftOn', SeparationQuotient.tendsto_lift_nhdsWithin_mk, SeparationQuotient.lift
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
s : Set (SeparationQuotient X)
⊢ ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s)

Tactic:
simp only [ContinuousOn, surjective_mk.forall, continuousWithinAt_lift, mem_preimage]

Premises used: Function.Surjective.forall, SeparationQuotient.continuousWithinAt_lift, SeparationQuotient.surjective_mk, ContinuousOn, Set.mem_preimage
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
⊢ Continuous[_, inst_1] (lift f hf) ↔ Continuous[inst, inst_1] f

Tactic:
simp only [← continuousOn_univ, continuousOn_lift, preimage_univ]

Premises used: SeparationQuotient.continuousOn_lift, Set.preimage_univ, continuousOn_univ
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
⊢ lift₂ f hf (mk x) (mk y) = f x y

Tactic:
rfl

Premises used: SeparationQuotient.lift₂, rfl, Quotient.liftOn₂'
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
rw : Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
rw [← map_prod_map_mk_nhds, tendsto_map'_iff]

Premises used: Filter.tendsto_map'_iff, SeparationQuotient.map_prod_map_mk_nhds
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf) ∘ Prod.map mk mk) (𝓝 (x, y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l

Tactic:
rfl
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))
l : Filter α
rw :
  Tendsto (uncurry (lift₂ f hf)) (map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
⊢ Tendsto (uncurry (lift₂ f hf)) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
rw [nhdsWithin, ← map_prod_map_mk_nhds, ← Filter.push_pull, comap_principal]

Premises used: nhdsWithin, Filter.push_pull, Filter.comap_principal, SeparationQuotient.map_prod_map_mk_nhds
-- Module: Mathlib.Topology.Inseparable
Goal:
X : Type u_1
Y : Type u_2
α : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y → α
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
s : Set (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))
l : Filter α
⊢ Tendsto (uncurry (lift₂ f hf)) (map (Prod.map mk mk) (𝓝 (x, y) ⊓ 𝓟 (Prod.map mk mk ⁻¹' s))) l ↔
    Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l

Tactic:
rfl
-- 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 → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
x : X
y : Y
⊢ ContinuousAt (uncurry (lift₂ f hf)) (mk x, mk y) ↔ ContinuousAt (uncurry f) (x, y)

Tactic:
tendsto_lift₂_nhds

Premises used: SeparationQuotient.tendsto_lift₂_nhds, ContinuousAt, SeparationQuotient.lift₂, Quotient, SeparationQuotient, Quotient.liftOn₂'
-- 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 → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (Prod.{u_1, u_2} (SeparationQuotient X) (SeparationQuotient Y))
x : X
y : Y
⊢ ContinuousWithinAt (uncurry (lift₂ f hf)) s (mk x, mk y) ↔
    ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (x, y)

Tactic:
tendsto_lift₂_nhdsWithin

Premises used: ContinuousWithinAt, SeparationQuotient.tendsto_lift₂_nhdsWithin, SeparationQuotient.lift₂, Quotient, SeparationQuotient, Quotient.liftOn₂'