awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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)
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
have mp : ∀ (x y : Completion α) (hxy : dist x y < ε), (x, y) ∈ s
Tactic: refine ⟨ε, εpos, @fun x y hxy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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
have refine_1 : IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t}
Tactic: refine induction_on₂ x y ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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}
⊢ ε ≤ dist x y ∨ (x, y) ∈ t
have refine_2 : ∀ (a b : α),
  ε ≤ dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) ∨ ((↑a : Completion α), (↑b : Completion α)) ∈ t
Tactic: refine induction_on₂ x y ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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 < ε
⊢ IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t}
have this : {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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 α) {x : Completion α × Completion α | ε ≤ dist x.1 x.2 ∨ (x.1, x.2) ∈ t}
have refine_1 : IsClosed ({p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 ({p : Completion α × Completion α | ε ≤ dist p.1 p.2} ∪ t)
have apply : IsClosed.{u} (X := Completion α × Completion α) {p : Completion α × Completion α | ε ≤ dist p.1 p.2}
Tactic: apply IsClosed.union _ tclosed
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 : α
⊢ ε ≤ dist (α := Completion α) (↑x : Completion α) (↑y : Completion α) ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
have refine_2 : ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
Tactic: rw [Completion.dist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 : α
⊢ ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
have pos : ∀ (h : ε ≤ dist x y), ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
Tactic: by_cases! h : ε ≤ dist x y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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
⊢ ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
have neg : ∀ (h : dist x y < ε), ε ≤ dist x y ∨ ((↑x : Completion α), (↑y : Completion α)) ∈ t
Tactic: by_cases! h : ε ≤ dist x y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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
have Z : Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (x, y)
Tactic: have Z := hε h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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, y) ∈ s
have this : ε ≤ 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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) ∈ s
have this₁ : (x, y) ∈ t
Tactic: simp only [not_le.mpr hxy, false_or] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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 < ε}
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
have this : r ∈ 𝓤 ℝ
Tactic: have : r ∈ uniformity ℝ := Metric.dist_mem_uniformity εpos
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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 α)) s
have 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}
Tactic: have T := uniformContinuous_def.1 (@Completion.uniformContinuous_dist α _) r this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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}
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
have 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}
Tactic: simp only [uniformity_prod_eq_prod, mem_prod_iff, Filter.mem_map] at T
Cleared hypotheses: T
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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}
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
have 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
Tactic: rcases T with ⟨t1, ht1, t2, ht2, ht⟩
Cleared hypotheses: T
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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
have mpr : t1 ⊆ s
Tactic: refine mem_of_superset ht1 ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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}
a b : Completion α
hab : (a, b) ∈ t1
⊢ dist a b < ε
have this₁ : ((a, b), a, a) ∈ t1 ×ˢ t2
Tactic: have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
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}
⊢ t1 ⊆ s
have A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
Tactic: have A : ∀ a b : Completion α, (a, b) ∈ t1 → dist a b < ε := by
      intro a b hab
      have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
      exact lt_of_le_of_lt (le_abs_self _)
        (by simpa [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] using ht this)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ Eq.{u + 1} (α := Filter (Completion α × Completion α)) (𝓤 (Completion α))
    (⨅ (ε : { ε : ℝ // 0 < ε }), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)})
have h : ∀ (s : Set (Completion α × Completion α)),
  Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    Membership.mem (γ := Filter (Completion α × Completion α))
      (⨅ (ε : { ε : ℝ // 0 < ε }), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)}) s
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    Membership.mem (γ := Filter (Completion α × Completion α))
      (⨅ (ε : { ε : ℝ // 0 < ε }), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)}) s
have h : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
  ∃ (i : { ε : ℝ // 0 < ε }),
    Membership.mem (γ := Filter (Completion α × Completion α))
      (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑i : ℝ)}) s
Tactic: rw [mem_iInf_of_directed]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
h :
  Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    ∃ (i : { ε : ℝ // 0 < ε }),
      Membership.mem (γ := Filter (Completion α × Completion α))
        (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑i : ℝ)}) s
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    Membership.mem (γ := Filter (Completion α × Completion α))
      (⨅ (ε : { ε : ℝ // 0 < ε }), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)}) s
have h₁ : Directed (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2) fun (ε : { ε : ℝ // 0 < ε }) ↦
  𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)}
Tactic: rw [mem_iInf_of_directed]