awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
this : x = y
rwa rwa₁ rwa₂ rwa₃ : y ∈ s
⊢ x ∈ s

Tactic:
rwa [this]
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
h : x = y
⊢ x ∈ s

Tactic:
suffices x = y by rwa [this]
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (x, y) ∈ V
⊢ x = y

Tactic:
apply eq_of_forall_symmetric

Premises used: eq_of_forall_symmetric
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V → (x, y) ∈ V
⊢ SetRel.IsSymm V → (x, y) ∈ V

Tactic:
_
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h_1 : SetRel.IsSymm V
h : ∀ (z : α) (hz : z ∈ ball x (V₁ ∩ V)) (hz' : z ∈ s), (x, y) ∈ V
⊢ (x, y) ∈ V

Tactic:
rcases hx (inter_mem V₁_in V_in) with ⟨z, hz, hz'⟩

Premises used: Filter.inter_mem
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
by_contra : ∀ (hzy : ¬z = y), False
⊢ z = y

Tactic:
by_contra hzy
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False

Tactic:
hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball (ball_inter_left x _ _ hz) hy)

Premises used: UniformSpace.mem_comp_of_mem_ball, UniformSpace.ball_inter_left
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hzy : ¬z = y
⊢ False

Tactic:
exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball (ball_inter_left x _ _ hz) hy)

Premises used: UniformSpace.mem_comp_of_mem_ball, UniformSpace.ball_inter_left
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
h_1 : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
h : ∀ (hy : z ∈ ball x V₁) (hy' : z ∈ s), (x, z) ∈ V
⊢ (x, y) ∈ V

Tactic:
obtain rfl : z = y := by
    by_contra hzy
    exact hs hz' hy' hzy (h_comp <| mem_comp_of_mem_ball (ball_inter_left x _ _ hz) hy)

Premises used: rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hy : z ∈ ball x V₁
hy' : z ∈ s
⊢ (x, z) ∈ V

Tactic:
ball_inter_right x _ _ hz

Premises used: Set.Mem, UniformSpace.ball_inter_right, setOf, UniformSpace.ball, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun (x y : α) ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
V : Set (α × α)
V_in : V ∈ 𝓤 α
h : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
hy : z ∈ ball x V₁
hy' : z ∈ s
⊢ (x, z) ∈ V

Tactic:
exact ball_inter_right x _ _ hz

Premises used: UniformSpace.ball_inter_right
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun (x y : ι) ↦ (f x, f y) ∉ V₀
x y : ι
h : f x ≠ f y
⊢ (f x, f y) ∉ V₀

Tactic:
hf (ne_of_apply_ne f h)

Premises used: ne_of_apply_ne
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
ι : Type u_1
inst_1 : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun (x y : ι) ↦ (f x, f y) ∉ V₀
x y : ι
h : f x ≠ f y
⊢ (f x, f y) ∉ V₀

Tactic:
exact hf (ne_of_apply_ne f h)

Premises used: ne_of_apply_ne
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α

Tactic:
le_antisymm ?_ le_comap_map

Premises used: le_antisymm, Filter.le_comap_map
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
refine :
  Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α
⊢ Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α

Tactic:
refine le_antisymm ?_ le_comap_map

Premises used: le_antisymm, Filter.le_comap_map
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α

Tactic:
((((𝓤 α).basis_sets.map _).comap _).le_basis_iff uniformity_hasBasis_open).2 fun U hU ↦ ?_

Premises used: Iff.mpr, uniformity, Filter.HasBasis.le_basis_iff, Filter.HasBasis.map, Filter.HasBasis.comap, Filter.basis_sets, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
refine :
  ∀ (U : SetRel α α) (hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U),
    ∃ i ∈ 𝓤 α,
      preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id i) ⊆ id U
⊢ Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α

Tactic:
refine ((((𝓤 α).basis_sets.map _).comap _).le_basis_iff uniformity_hasBasis_open).2 fun U hU ↦ ?_

Premises used: Iff.mpr, uniformity, Filter.HasBasis.le_basis_iff, Filter.HasBasis.map, Filter.HasBasis.comap, Filter.basis_sets, uniformity_hasBasis_open
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
⊢ ∃ i ∈ 𝓤 α,
    preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id i) ⊆ id U

Tactic:
⟨U, hU.1, fun (x₁, x₂) ⟨(y₁, y₂), hyU, hxy⟩ ↦ ?_⟩

Premises used: _private.0.SeparationQuotient.comap_map_mk_uniformity.match_1, Membership.mem, id, Prod.mk, _private.0.SeparationQuotient.comap_map_mk_uniformity.match_2, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
refine :
  ∀ (x : α × α) (x₁ x₂ : α),
    (x₁, x₂) ∈ preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id U) →
      ∀ (y₁ y₂ : α) (hyU : (y₁, y₂) ∈ id U)
        (hxy :
          Eq (α := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk (y₁, y₂)) (Prod.map mk mk (x₁, x₂))),
        (x₁, x₂) ∈ id U
⊢ ∃ i ∈ 𝓤 α,
    preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id i) ⊆ id U

Tactic:
refine ⟨U, hU.1, fun (x₁, x₂) ⟨(y₁, y₂), hyU, hxy⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
x : α × α
x₁ x₂ : α
h : (x₁, x₂) ∈ preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Eq (α := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk (y₁, y₂)) (Prod.map mk mk (x₁, x₂))
⊢ Inseparable y₁ x₁ ∧ Inseparable y₂ x₂

Tactic:
simp only [Prod.map, Prod.ext_iff, mk_eq_mk] at hxy

Premises used: SeparationQuotient.mk_eq_mk, Prod.ext_iff, Prod.map
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
x : α × α
x₁ x₂ : α
h : (x₁, x₂) ∈ preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Inseparable y₁ x₁ ∧ Inseparable y₂ x₂
⊢ (x₁, x₂) ∈ id U

Tactic:
((hxy.1.prod hxy.2).mem_open_iff hU.2).1 hyU

Premises used: Set.Mem, And.right, And.left, Iff.mp, Inseparable.prod, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] U
x : α × α
x₁ x₂ : α
h : (x₁, x₂) ∈ preimage (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Inseparable y₁ x₁ ∧ Inseparable y₂ x₂
⊢ (x₁, x₂) ∈ id U

Tactic:
exact ((hxy.1.prod hxy.2).mem_open_iff hU.2).1 hyU

Premises used: And.right, And.left, Iff.mp, Inseparable.prod, Inseparable.mem_open_iff
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
rcases :
  ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α) (hUo : IsOpen[instTopologicalSpaceProd] U)
    (hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t),
    Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α))
      (Filter.lift' (α := SeparationQuotient α × SeparationQuotient α) (map (Prod.map mk mk) (𝓤 α))
        fun (s : Set (SeparationQuotient α × SeparationQuotient α)) ↦ SetRel.comp s s)
      t
⊢ Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α))
    (Filter.lift' (α := SeparationQuotient α × SeparationQuotient α) (map (Prod.map mk mk) (𝓤 α))
      fun (s : Set (SeparationQuotient α × SeparationQuotient α)) ↦ SetRel.comp s s)
    t

Tactic:
rcases comp_open_symm_mem_uniformity_sets ht with ⟨U, hU, hUo, -, hUt⟩

Premises used: comp_open_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
⊢ Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α))
    (Filter.lift' (α := SeparationQuotient α × SeparationQuotient α) (map (Prod.map mk mk) (𝓤 α))
      fun (s : Set (SeparationQuotient α × SeparationQuotient α)) ↦ SetRel.comp s s)
    t

Tactic:
mem_of_superset (mem_lift' <| image_mem_map hU) ?_

Premises used: Filter.image_mem_map, Filter.mem_lift', Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
refine : SetRel.comp (β := SeparationQuotient α) (Prod.map mk mk '' U) (Prod.map mk mk '' U) ⊆ t
⊢ Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α))
    (Filter.lift' (α := SeparationQuotient α × SeparationQuotient α) (map (Prod.map mk mk) (𝓤 α))
      fun (s : Set (SeparationQuotient α × SeparationQuotient α)) ↦ SetRel.comp s s)
    t

Tactic:
refine mem_of_superset (mem_lift' <| image_mem_map hU) ?_

Premises used: Filter.image_mem_map, Filter.mem_lift', Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
simp :
  ∀ (a b : SeparationQuotient α),
    (∃ (b_1 : SeparationQuotient α),
        (∃ x ∈ U, (Prod.map mk mk x).1 = a ∧ (Prod.map mk mk x).2 = b_1) ∧
          ∃ x ∈ U, (Prod.map mk mk x).1 = b_1 ∧ (Prod.map mk mk x).2 = b) →
      (a, b) ∈ t
⊢ SetRel.comp (β := SeparationQuotient α) (Prod.map mk mk '' U) (Prod.map mk mk '' U) ⊆ t

Tactic:
simp only [subset_def, Prod.forall, SetRel.mem_comp, mem_image, Prod.ext_iff]

Premises used: SetRel.mem_comp, Set.subset_def, Set.mem_image, Prod.ext_iff, Prod.forall
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : Eq (α := SeparationQuotient α) (Prod.map mk mk (y', z)).1 (Prod.map mk mk (x, y)).2
⊢ y' ⤳ y

Tactic:
have : y' ⤳ y := (mk_eq_mk.1 hy).specializes
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : Eq (α := SeparationQuotient α) (Prod.map mk mk (y', z)).1 (Prod.map mk mk (x, y)).2
this : y' ⤳ y
⊢ ((Prod.map mk mk (x, y)).1, (Prod.map mk mk (y', z)).2) ∈ t

Tactic:
@hUt (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩

Premises used: Set.Mem, Specializes.mem_open, setOf, UniformSpace.isOpen_ball, Prod.map, Set.preimage, And.intro, SeparationQuotient.mk, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : Eq (α := SeparationQuotient α) (Prod.map mk mk (y', z)).1 (Prod.map mk mk (x, y)).2
this : y' ⤳ y
⊢ ((Prod.map mk mk (x, y)).1, (Prod.map mk mk (y', z)).2) ∈ t

Tactic:
exact @hUt (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩

Premises used: Specializes.mem_open, UniformSpace.isOpen_ball, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
x : α
rw :
  Filter.comap (Prod.mk x)
    (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)))
| Filter.comap (β := SeparationQuotient α) mk (𝓝 (mk x))

Tactic:
rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]

Premises used: SeparationQuotient.comap_mk_nhds_mk, SeparationQuotient.comap_map_mk_uniformity, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
x : α
conv_lhs :
  Filter.comap (Prod.mk x)
      (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α))) =
    Filter.comap (β := SeparationQuotient α) mk
      (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))
⊢ Filter.comap (β := SeparationQuotient α) mk (𝓝 (mk x)) =
    Filter.comap (β := SeparationQuotient α) mk
      (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))

Tactic:
conv_lhs => rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]

Premises used: SeparationQuotient.comap_mk_nhds_mk, SeparationQuotient.comap_map_mk_uniformity, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
x : α
⊢ Filter.comap (Prod.mk x)
      (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α))) =
    Filter.comap (β := SeparationQuotient α) mk
      (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))

Tactic:
simp only [Filter.comap_comap, Function.comp_def, Prod.map_apply]

Premises used: Function.comp_def, Filter.comap_comap, Prod.map_apply
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ Eq (α := Filter (SeparationQuotient α × SeparationQuotient α)) (𝓤 (SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α))

Tactic:
rfl

Premises used: Filter.map, uniformity, rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
inst : UniformSpace α
⊢ UniformContinuous.{u, u} (α := α) (β := SeparationQuotient α) mk

Tactic:
le_rfl

Premises used: UniformContinuous, le_rfl, Set.Mem, Prod.map, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : SeparationQuotient α → β
⊢ UniformContinuous f ↔ UniformContinuous (f ∘ mk)

Tactic:
.rfl

Premises used: UniformContinuous, Set.Mem, Iff.rfl, setOf, Prod.map, Quotient, Set.preimage, Filter.Tendsto, SeparationQuotient, SeparationQuotient.mk
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β) → γ
simp :
  Tendsto
      (comp (β :=
        Prod.{u, v} (SeparationQuotient α × SeparationQuotient α) (SeparationQuotient β × SeparationQuotient β))
        ((fun
              (x :
                Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β) ×
                  Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β)) ↦
            (f x.1, f x.2)) ∘
          fun
            (p :
              Prod.{u, v} (SeparationQuotient α × SeparationQuotient α) (SeparationQuotient β × SeparationQuotient β)) ↦
          ((p.1.1, p.2.1), p.1.2, p.2.2))
        fun (p : Prod.{u, v} (α × α) (β × β)) ↦ (Prod.map mk mk p.1, Prod.map mk mk p.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ) ↔
    Tendsto
      ((fun (x : (α × β) × α × β) ↦ (f (mk x.1.1, mk x.1.2), f (mk x.2.1, mk x.2.2))) ∘
        fun (p : Prod.{u, v} (α × α) (β × β)) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)
⊢ UniformContinuous f ↔ UniformContinuous (β := γ) fun (p : α × β) ↦ f (mk p.1, mk p.2)

Tactic:
simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq, prod_map_map_eq,
    tendsto_map'_iff]

Premises used: UniformContinuous, SeparationQuotient.uniformity_eq, Filter.tendsto_map'_iff, uniformity_prod_eq_prod, Filter.prod_map_map_eq
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β) → γ
⊢ Tendsto
      (comp (β :=
        Prod.{u, v} (SeparationQuotient α × SeparationQuotient α) (SeparationQuotient β × SeparationQuotient β))
        ((fun
              (x :
                Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β) ×
                  Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β)) ↦
            (f x.1, f x.2)) ∘
          fun
            (p :
              Prod.{u, v} (SeparationQuotient α × SeparationQuotient α) (SeparationQuotient β × SeparationQuotient β)) ↦
          ((p.1.1, p.2.1), p.1.2, p.2.2))
        fun (p : Prod.{u, v} (α × α) (β × β)) ↦ (Prod.map mk mk p.1, Prod.map mk mk p.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ) ↔
    Tendsto
      ((fun (x : (α × β) × α × β) ↦ (f (mk x.1.1, mk x.1.2), f (mk x.2.1, mk x.2.2))) ∘
        fun (p : Prod.{u, v} (α × α) (β × β)) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Separation
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : ∀ (a b : α), Inseparable a b → f a = f b
⊢ UniformContinuous (lift f h) ↔ UniformContinuous f

Tactic:
.rfl

Premises used: UniformContinuous, Quotient.liftOn', Set.Mem, Iff.rfl, setOf, Prod.map, Quotient, Set.preimage, Filter.Tendsto, SeparationQuotient, SeparationQuotient.mk, SeparationQuotient.lift