awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
mp : ∀ (x y : Completion α) (hxy : dist x y < ε), (x, y) ∈ s
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
refine ⟨ε, εpos, @fun x y hxy ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
⊢ ε ≤ dist x y ∨ (x, y) ∈ t

Tactic:
induction_on₂ x y ?_ ?_

Premises used: UniformSpace.Completion.induction_on₂
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
refine_1 :
  IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t}
refine_2 :
  ∀ (a b : α),
    ε ≤ dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) ∨
      ((↑a : Completion α), (↑b : Completion α)) ∈ t
⊢ ε ≤ dist x y ∨ (x, y) ∈ t

Tactic:
refine induction_on₂ x y ?_ ?_
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
h :
  ∀ (x : Completion α × Completion α),
    Membership.mem (γ := Set (Completion α × Completion α))
        {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} x ↔
      x ∈ {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t
⊢ {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
x_1 : Completion α × Completion α
⊢ Membership.mem (γ := Set (Completion α × Completion α))
      {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} x_1 ↔
    x_1 ∈ {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
⊢ {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t

Tactic:
have : { x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t } =
               { p : Completion α × Completion α | ε ≤ dist p.1 p.2 } ∪ t := by ext; simp
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
this :
  {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t
refine_1 : IsClosed ({p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t)
⊢ IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t}

Tactic:
rw [this]
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
this :
  {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t
apply : IsClosed.{u} (X := Completion α × Completion α) {p : Completion α × Completion α | ε ≤ dist p.1 p.2}
⊢ IsClosed ({p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t)

Tactic:
apply IsClosed.union _ tclosed

Premises used: IsClosed.union
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
this :
  {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t
⊢ IsClosed.{u} (X := Completion α × Completion α) {p : Completion α × Completion α | ε ≤ dist p.1 p.2}

Tactic:
isClosed_le continuous_const Completion.uniformContinuous_dist.continuous

Premises used: UniformSpace.Completion.uniformContinuous_dist, continuous_const, setOf, isClosed_le, UniformContinuous.continuous
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
this :
  {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t} =
    {p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t
⊢ IsClosed.{u} (X := Completion α × Completion α) {p : Completion α × Completion α | ε ≤ dist p.1 p.2}

Tactic:
exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous

Premises used: UniformSpace.Completion.uniformContinuous_dist, continuous_const, isClosed_le, UniformContinuous.continuous
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x_1 y_1 : Completion α
hxy : dist x_1 y_1 < ε
x y : α
refine_2 : ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
⊢ ε ≤ dist (α := Completion α) (↑x : Completion α) (↑y : Completion α) ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t

Tactic:
rw [Completion.dist_eq]

Premises used: UniformSpace.Completion.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x_1 y_1 : Completion α
hxy : dist x_1 y_1 < ε
x y : α
pos : ∀ (h : ε ≤ dist x y), ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
neg : ∀ (h : dist x y < ε), ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
⊢ ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t

Tactic:
by_cases! h : ε ≤ dist x y

Premises used: Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x_1 y_1 : Completion α
hxy : dist x_1 y_1 < ε
x y : α
h : ε ≤ dist x y
⊢ ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x_1 y_1 : Completion α
hxy : dist x_1 y_1 < ε
x y : α
h : ε ≤ dist x y
⊢ ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t

Tactic:
exact Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x_1 y_1 : Completion α
hxy : dist x_1 y_1 < ε
x y : α
h : dist x y < ε
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (x, y)

Tactic:
have Z := hε h
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x_1 y_1 : Completion α
hxy : dist x_1 y_1 < ε
x y : α
h : dist x y < ε
Z : ((↑x : Completion α), (↑y : Completion α)) ∈ t
⊢ ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t

Tactic:
Or.inr Z

Premises used: Or.inr
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x_1 y_1 : Completion α
hxy : dist x_1 y_1 < ε
x y : α
h : dist x y < ε
Z : ((↑x : Completion α), (↑y : Completion α)) ∈ t
⊢ ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t

Tactic:
exact Or.inr Z

Premises used: Or.inr
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
⊢ ε ≤ dist x y ∨ (x, y) ∈ t

Tactic:
have : ε ≤ dist x y ∨ (x, y) ∈ t := by
      refine induction_on₂ x y ?_ ?_
      · have : { x : Completion α × Completion α | ε ≤ dist x.fst x.snd ∨ (x.fst, x.snd) ∈ t } =
               { p : Completion α × Completion α | ε ≤ dist p.1 p.2 } ∪ t := by ext; simp
        rw [this]
        apply IsClosed.union _ tclosed
        exact isClosed_le continuous_const Completion.uniformContinuous_dist.continuous
      · intro x y
        rw [Completion.dist_eq]
        by_cases! h : ε ≤ dist x y
        · exact Or.inl h
        · have Z := hε h
          simp only [Set.mem_setOf_eq] at Z
          exact Or.inr Z
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
this : ε ≤ dist x y ∨ (x, y) ∈ t
⊢ (x, y) ∈ t

Tactic:
simp only [not_le.mpr hxy, false_or] at this

Premises used: not_le, Iff.mpr, false_or
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
this : (x, y) ∈ t
⊢ (x, y) ∈ s

Tactic:
ts this
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε :
  ∀ ⦃a b : α⦄,
    dist a b < ε →
      Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)
x y : Completion α
hxy : dist x y < ε
this : (x, y) ∈ t
⊢ (x, y) ∈ s

Tactic:
exact ts this
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
⊢ r ∈ 𝓤 ℝ

Tactic:
have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
⊢ Membership.mem (γ := Filter ((Completion α × Completion α) × Completion α × Completion α))
    (𝓤 (Completion α × Completion α))
    {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}

Tactic:
have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
T :
  Membership.mem (γ := Filter ((Completion α × Completion α) × Completion α × Completion α))
    (𝓤 (Completion α × Completion α))
    {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
⊢ ∃ (t₁ : Set (Completion α × Completion α)),
    Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t₁ ∧
      ∃ (t₂ : Set (Completion α × Completion α)),
        Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t₂ ∧
          t₁ ×ˢ t₂ ⊆
            preimage (β := (Completion α × Completion α) × Completion α × Completion α)
              (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
              {x : (Completion α × Completion α) × Completion α × Completion α |
                (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}

Tactic:
simp only [uniformity_prod_eq_prod, mem_prod_iff, Filter.mem_map] at T

Premises used: uniformity_prod_eq_prod, Filter.mem_prod_iff, Filter.mem_map
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
T :
  ∃ (t₁ : Set (Completion α × Completion α)),
    Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t₁ ∧
      ∃ (t₂ : Set (Completion α × Completion α)),
        Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t₂ ∧
          t₁ ×ˢ t₂ ⊆
            preimage (β := (Completion α × Completion α) × Completion α × Completion α)
              (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
              {x : (Completion α × Completion α) × Completion α × Completion α |
                (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
mpr :
  ∀ (t1 : Set (Completion α × Completion α))
    (ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1)
    (t2 : Set (Completion α × Completion α))
    (ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2)
    (ht :
      t1 ×ˢ t2 ⊆
        preimage (β := (Completion α × Completion α) × Completion α × Completion α)
          (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
          {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}),
    Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s

Tactic:
rcases T with ⟨t1, ht1, t2, ht2, ht⟩
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1
t2 : Set (Completion α × Completion α)
ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2
ht :
  t1 ×ˢ t2 ⊆
    preimage (β := (Completion α × Completion α) × Completion α × Completion α)
      (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s

Tactic:
mem_of_superset ht1 ?_

Premises used: Filter.mem_of_superset