awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
⊢ ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
have refine : ∀ (x y : β) (hxy : dist x y < δ) (i : ι), dist (F i x) (F i y) < ε
Tactic: refine ⟨δ, δ0, fun x y hxy i => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (F i x) (F i y) < ε
have dist : |b (dist x y)| = dist (b (dist x y)) 0
Tactic: calc
    dist (F i x) (F i y) ≤ b (dist x y) := H x y i
    _ ≤ |b (dist x y)| := le_abs_self _
    _ = dist (b (dist x y)) 0 := by simp [Real.dist_eq]
    _ < ε := hδ (by simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
⊢ Eq (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
have A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
Tactic: have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => by positivity
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ Eq (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
have refine : LE.le (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
Tactic: refine le_antisymm ?_ (le_ciInf A)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ LE.le (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
have this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
Tactic: have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ LE.le (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
have rw : ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
have this : Eq (α := ℝ) (⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) 0
Tactic: have : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0 := by
    have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => by positivity
    refine le_antisymm ?_ (le_ciInf A)
    have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
    rw [this]
    exact ciInf_le ⟨0, forall_mem_range.2 A⟩ p
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inr z)
have simp : (⨅ (p : Z), dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ε + dist y z
Tactic: simp only [glueDist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ (p : Z), dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ε + dist y z
have rw : ⨅ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + dist y z
Tactic: rw [add_right_comm, add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ ⨅ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + dist y z
have refine_1 : ∀ (p : Z), Membership.mem (γ := Set ℝ) (lowerBounds (range fun (p : Z) ↦ dist x (Φ p) + dist z (Ψ p))) 0
Tactic: refine le_ciInf_add fun p => ciInf_le_of_le ⟨0, ?_⟩ p ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
refine_1 : ∀ (p : Z), Membership.mem (γ := Set ℝ) (lowerBounds (range fun (p : Z) ↦ dist x (Φ p) + dist z (Ψ p))) 0
⊢ ⨅ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + dist y z
have refine_2 : ∀ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z
Tactic: refine le_ciInf_add fun p => ciInf_le_of_le ⟨0, ?_⟩ p ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z
have linarith : dist x (Φ p) + dist y (Ψ p) + dist y z < dist x (Φ p) + dist z (Ψ p) →
  dist x (Φ p) + dist y (Ψ p) + dist y z - (dist x (Φ p) + dist z (Ψ p)) + (dist z (Ψ p) - (dist y z + dist y (Ψ p))) =
    0
Tactic: linarith [dist_triangle_left z (Ψ p) y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)
have simp_rw : dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
Tactic: simp_rw [glueDist, add_add_add_comm _ ε, add_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
have refine : ∀ (p : Z), dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
Tactic: refine le_ciInf_add fun p => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
have rw : dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
Tactic: rw [add_left_comm, add_assoc, ← two_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
have refine : ∀ (q : Z), dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
Tactic: refine le_ciInf_add fun q => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
have rw : dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
Tactic: rw [dist_comm z]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
have linarith : dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε)) < dist x z →
  dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε)) - dist x z +
          (dist x z - (dist x (Φ p) + dist (Φ p) (Φ q) + dist (Φ q) z)) +
        (dist (Ψ p) (Ψ q) - (dist y (Ψ p) + dist y (Ψ q))) +
      (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q) - 2 * ε) =
    0
Tactic: linarith [dist_triangle4 x (Φ p) (Φ q) z, dist_triangle_left (Ψ p) (Ψ q) y, (abs_le.1 (H p q)).2]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y z : X
⊢ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inl z)
have simp : glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl z)) ≤
  glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl y)) +
    glueDist Ψ Φ ε (Sum.swap (Sum.inl y)) (Sum.swap (Sum.inl z))
Tactic: simp only [← glueDist_swap Φ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y : X
z : Y
⊢ glueDist Φ Ψ ε (Sum.inr x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inr z)
have simp : glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inr z)) ≤
  glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl y)) +
    glueDist Ψ Φ ε (Sum.swap (Sum.inl y)) (Sum.swap (Sum.inr z))
Tactic: simp only [← glueDist_swap Φ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y : X
z : Y
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inr z)) ≤
    glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl y)) +
      glueDist Ψ Φ ε (Sum.swap (Sum.inl y)) (Sum.swap (Sum.inr z))
have H₁ : ∀ (p q : Z), |dist (Ψ p) (Ψ q) - dist (Φ p) (Φ q)| ≤ 2 * ε
Tactic: apply glueDist_triangle_inl_inr_inl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : X
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) = 0
⊢ Eq (α := X ⊕ Y) (Sum.inl x) (Sum.inl y)
have rw : Eq (α := X ⊕ Y) (Sum.inl y) (Sum.inl y)
Tactic: rw [eq_of_dist_eq_zero h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ Sum.inl x = Sum.inr y
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ False
have linarith : 0 - ε + (glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) - 0) + (ε - glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y)) = 0
Tactic: linarith [le_glueDist_inl_inr Φ Ψ ε x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ Sum.inr x = Sum.inl y
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ False
have linarith : 0 - ε + (glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) - 0) + (ε - glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)) = 0
Tactic: linarith [le_glueDist_inr_inl Φ Ψ ε x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : Y
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inr y) = 0
⊢ Eq (α := X ⊕ Y) (Sum.inr x) (Sum.inr y)
have rw : Eq (α := X ⊕ Y) (Sum.inr y) (Sum.inr y)
Tactic: rw [eq_of_dist_eq_zero h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s ↔
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
have simp : ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
    ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) ↔
  ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
Tactic: simp only [Sum.uniformity, Filter.mem_sup, Filter.mem_map, mem_uniformity_dist, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) ↔
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
have mp : ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
    ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) →
  ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
mp :
  ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) →
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
⊢ ((∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s) ↔
    ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
have mpr : (∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s) →
  (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
    ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
⊢ ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
have mp : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < min (min δX δY) ε → (a, b) ∈ s
Tactic: refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
a b : X
h : glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < min (min δX δY) ε
⊢ (Sum.inl a, Sum.inl b) ∈ s
have h₁ : (glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < δX ∧ glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < δY) ∧
  glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < ε
Tactic: simp only [lt_min_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
a : X
b : Y
h : glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < min (min δX δY) ε
⊢ (Sum.inl a, Sum.inr b) ∈ s
have h₁ : (glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < δX ∧ glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < δY) ∧
  glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < ε
Tactic: simp only [lt_min_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
a : Y
b : X
h : glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < min (min δX δY) ε
⊢ (Sum.inr a, Sum.inl b) ∈ s
have h₁ : (glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < δX ∧ glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < δY) ∧
  glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < ε
Tactic: simp only [lt_min_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ ⦃a b : X⦄, dist a b < δX → Prod.map Sum.inl Sum.inl (a, b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ ⦃a b : Y⦄, dist a b < δY → Prod.map Sum.inr Sum.inr (a, b) ∈ s
a b : Y
h : glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < min (min δX δY) ε
⊢ (Sum.inr a, Sum.inr b) ∈ s
have h₁ : (glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < δX ∧ glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < δY) ∧
  glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < ε
Tactic: simp only [lt_min_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε_1 : ℝ
hε : 0 < ε_1
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε_1 a b < ε → (a, b) ∈ s
⊢ (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
    ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s
have mpr : ∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε_1 : ℝ
hε : 0 < ε_1
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε_1 a b < ε → (a, b) ∈ s
mpr : ∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s
⊢ (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
    ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s
have mpr₁ : ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
p q : X ⊕ Y
x : X
y : Y
⊢ Sum.dist p q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 p q
have inl : ∀ (val : X), Sum.dist (Sum.inl val) q = glueDist (fun (x_1 : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inl val) q
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
p q : X ⊕ Y
x : X
y : Y
inl :
  ∀ (val : X),
    Sum.dist (Sum.inl val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) q
⊢ Sum.dist p q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 p q
have inr : ∀ (val : Y), Sum.dist (Sum.inr val) q = glueDist (fun (x_1 : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inr val) q
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
q : X ⊕ Y
x : X
y : Y
val : X
⊢ Sum.dist (Sum.inl val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) q
have inl : ∀ (val_1 : X),
  Sum.dist.{u, v} (Y := Y) (Sum.inl val) (Sum.inl val_1) =
    glueDist.{u, v, 0} (Y := Y) (fun (x_1 : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inl val) (Sum.inl val_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
q : X ⊕ Y
x : X
y : Y
val : X
inl :
  ∀ (val_1 : X),
    Sum.dist.{u, v} (Y := Y) (Sum.inl val) (Sum.inl val_1) =
      glueDist.{u, v, 0} (Y := Y) (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) (Sum.inl val_1)
⊢ Sum.dist (Sum.inl val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) q
have inl₁ : ∀ (val_1 : Y),
  Sum.dist (Sum.inl val) (Sum.inr val_1) =
    glueDist (fun (x_1 : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inl val) (Sum.inr val_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
q : X ⊕ Y
x : X
y val : Y
⊢ Sum.dist (Sum.inr val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) q
have inr : ∀ (val_1 : X),
  Sum.dist (Sum.inr val) (Sum.inl val_1) =
    glueDist (fun (x_1 : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inr val) (Sum.inl val_1)
Tactic: cases q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
q : X ⊕ Y
x : X
y val : Y
inr :
  ∀ (val_1 : X),
    Sum.dist (Sum.inr val) (Sum.inl val_1) =
      glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) (Sum.inl val_1)
⊢ Sum.dist (Sum.inr val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) q
have inr₁ : ∀ (val_1 : Y),
  Sum.dist.{u, v} (X := X) (Sum.inr val) (Sum.inr val_1) =
    glueDist.{u, v, 0} (X := X) (fun (x_1 : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inr val) (Sum.inr val_1)
Tactic: cases q
Cleared hypotheses: q