awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
⊢ Sum.dist x y = Sum.dist y x
have inl : ∀ (val : X), Sum.dist (Sum.inl val) y = Sum.dist y (Sum.inl val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inl : ∀ (val : X), Sum.dist (Sum.inl val) y = Sum.dist y (Sum.inl val)
⊢ Sum.dist x y = Sum.dist y x
have inr : ∀ (val : Y), Sum.dist (Sum.inr val) y = Sum.dist y (Sum.inr val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
y : X ⊕ Y
val : X
⊢ Sum.dist (Sum.inl val) y = Sum.dist y (Sum.inl val)
have inl : ∀ (val_1 : X),
  Sum.dist.{u, v} (Y := Y) (Sum.inl val) (Sum.inl val_1) = Sum.dist.{u, v} (Y := Y) (Sum.inl val_1) (Sum.inl val)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
y : X ⊕ Y
val : X
inl :
  ∀ (val_1 : X),
    Sum.dist.{u, v} (Y := Y) (Sum.inl val) (Sum.inl val_1) = Sum.dist.{u, v} (Y := Y) (Sum.inl val_1) (Sum.inl val)
⊢ Sum.dist (Sum.inl val) y = Sum.dist y (Sum.inl val)
have inl₁ : ∀ (val_1 : Y), Sum.dist (Sum.inl val) (Sum.inr val_1) = Sum.dist (Sum.inr val_1) (Sum.inl val)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
y : X ⊕ Y
val : Y
⊢ Sum.dist (Sum.inr val) y = Sum.dist y (Sum.inr val)
have inr : ∀ (val_1 : X), Sum.dist (Sum.inr val) (Sum.inl val_1) = Sum.dist (Sum.inl val_1) (Sum.inr val)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
y : X ⊕ Y
val : Y
inr : ∀ (val_1 : X), Sum.dist (Sum.inr val) (Sum.inl val_1) = Sum.dist (Sum.inl val_1) (Sum.inr val)
⊢ Sum.dist (Sum.inr val) y = Sum.dist y (Sum.inr val)
have inr₁ : ∀ (val_1 : Y),
  Sum.dist.{u, v} (X := X) (Sum.inr val) (Sum.inr val_1) = Sum.dist.{u, v} (X := X) (Sum.inr val_1) (Sum.inr val)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
have grw : 1 ≤ dist x sorry.some + 1 + dist sorry.some y
Tactic: grw [Sum.dist, ← le_add_of_nonneg_right dist_nonneg, ← le_add_of_nonneg_left dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y : Y
grw : 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
have grw₁ : 1 ≤ dist x sorry.some + 1
Tactic: grw [Sum.dist, ← le_add_of_nonneg_right dist_nonneg, ← le_add_of_nonneg_left dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y : Y
grw : 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y
grw₁ : 1 ≤ dist x ⋯.some + 1
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
have grw₂ : LE.le (α := ℝ) 1 1
Tactic: grw [Sum.dist, ← le_add_of_nonneg_right dist_nonneg, ← le_add_of_nonneg_left dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inr y) (Sum.inl x)
have rw : 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
Tactic: rw [Sum.dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s ↔
    ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
have mp : Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s → ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (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
s : Set ((X ⊕ Y) × (X ⊕ Y))
mp :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s →
    ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s ↔
    ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
have mpr : (∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) →
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) 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
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)) s
hsY :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)) s
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
have mp : ∀ (εX : ℝ) (εX0 : εX > 0)
  (hX :
    ∀ ⦃a b : X⦄,
      dist a b < εX → Membership.mem (γ := Set (X × X)) ((fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s) (a, b)),
  ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
Tactic: rcases mem_uniformity_dist.1 hsX with ⟨εX, εX0, hX⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)) s
hsY :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)) s
εX : ℝ
εX0 : εX > 0
hX :
  ∀ ⦃a b : X⦄,
    dist a b < εX → Membership.mem (γ := Set (X × X)) ((fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s) (a, b)
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
have mp : ∀ (εY : ℝ) (εY0 : εY > 0)
  (hY :
    ∀ ⦃a b : Y⦄,
      dist a b < εY → Membership.mem (γ := Set (Y × Y)) ((fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s) (a, b)),
  ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
Tactic: rcases mem_uniformity_dist.1 hsY with ⟨εY, εY0, hY⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)) s
hsY :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)) s
εX : ℝ
εX0 : εX > 0
hX :
  ∀ ⦃a b : X⦄,
    dist a b < εX → Membership.mem (γ := Set (X × X)) ((fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s) (a, b)
εY : ℝ
εY0 : εY > 0
hY :
  ∀ ⦃a b : Y⦄,
    dist a b < εY → Membership.mem (γ := Set (Y × Y)) ((fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s) (a, b)
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
have mp : ∀ (a b : X ⊕ Y), Sum.dist a b < min (min εX εY) 1 → (a, b) ∈ s
Tactic: refine ⟨min (min εX εY) 1, lt_min (lt_min εX0 εY0) zero_lt_one, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s
have mpr : Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)) 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
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
mpr :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)) s
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s
have mpr₁ : Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)) 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
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)) s
have mpr : ∃ ε > 0,
  ∀ ⦃a b : X⦄,
    dist a b < ε → Membership.mem (γ := Set (X × X)) ((fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) ⁻¹' s) (a, b)
Tactic: rw [Filter.mem_map, mem_uniformity_dist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)) s
have mpr : ∃ ε > 0,
  ∀ ⦃a b : Y⦄,
    dist a b < ε → Membership.mem (γ := Set (Y × Y)) ((fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) ⁻¹' s) (a, b)
Tactic: rw [Filter.mem_map, mem_uniformity_dist]
-- 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
x : X ⊕ Y
⊢ Sum.dist x x = 0
have inl : ∀ (val : X), Sum.dist.{u, v} (Y := Y) (Sum.inl val) (Sum.inl val) = 0
Tactic: cases x
Cleared hypotheses: x
-- 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
x : X ⊕ Y
inl : ∀ (val : X), Sum.dist.{u, v} (Y := Y) (Sum.inl val) (Sum.inl val) = 0
⊢ Sum.dist x x = 0
have inr : ∀ (val : Y), Sum.dist.{u, v} (X := X) (Sum.inr val) (Sum.inr val) = 0
Tactic: cases x
Cleared hypotheses: x
-- 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
p : X
q : Y
x : X ⊕ Y
⊢ Sum.dist (Sum.inl p) x ≤ Sum.dist (Sum.inl p) (Sum.inr q) + Sum.dist (Sum.inr q) x
have simp : glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inl p) x ≤
  glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inl p) (Sum.inr q) +
    glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inr q) x
Tactic: simp only [Sum.dist_eq_glueDist p 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
x : X ⊕ Y
q : X
r : Y
⊢ Sum.dist x (Sum.inr r) ≤ Sum.dist x (Sum.inl q) + Sum.dist (Sum.inl q) (Sum.inr r)
have simp : glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 x (Sum.inr r) ≤
  glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 x (Sum.inl q) +
    glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inl q) (Sum.inr r)
Tactic: simp only [Sum.dist_eq_glueDist q r]
-- 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
p : Y
x : X ⊕ Y
r : X
⊢ Sum.dist (Sum.inr p) (Sum.inl r) ≤ Sum.dist (Sum.inr p) x + Sum.dist x (Sum.inl r)
have simp : glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inr p) (Sum.inl r) ≤
  glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 (Sum.inr p) x +
    glueDist (fun (x : Unit) ↦ sorry.some) (fun (x : Unit) ↦ sorry.some) 1 x (Sum.inl r)
Tactic: simp only [Sum.dist_eq_glueDist r 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
p q : X ⊕ Y
h : Sum.dist p q = 0
⊢ p = q
have inl : ∀ (p : X) (h : Sum.dist (Sum.inl p) q = 0), Sum.inl p = q
Tactic: rcases p with p | p
Cleared hypotheses: p, 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
p q : X ⊕ Y
h : Sum.dist p q = 0
inl : ∀ (p : X) (h : Sum.dist (Sum.inl p) q = 0), Sum.inl p = q
⊢ p = q
have inr : ∀ (p : Y) (h : Sum.dist (Sum.inr p) q = 0), Sum.inr p = q
Tactic: rcases p with p | p
Cleared hypotheses: p, 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
q : X ⊕ Y
p : X
h : Sum.dist (Sum.inl p) q = 0
⊢ Sum.inl p = q
have inl : ∀ (q : X) (h : Sum.dist.{u, v} (Y := Y) (Sum.inl p) (Sum.inl q) = 0), Eq (α := X ⊕ Y) (Sum.inl p) (Sum.inl q)
Tactic: rcases q with q | q
Cleared hypotheses: q, 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
q : X ⊕ Y
p : X
h : Sum.dist (Sum.inl p) q = 0
inl : ∀ (q : X) (h : Sum.dist.{u, v} (Y := Y) (Sum.inl p) (Sum.inl q) = 0), Eq (α := X ⊕ Y) (Sum.inl p) (Sum.inl q)
⊢ Sum.inl p = q
have inl₁ : ∀ (q : Y) (h : Sum.dist (Sum.inl p) (Sum.inr q) = 0), Sum.inl p = Sum.inr q
Tactic: rcases q with q | q
Cleared hypotheses: q, 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
q : X ⊕ Y
p : Y
h : Sum.dist (Sum.inr p) q = 0
⊢ Sum.inr p = q
have inr : ∀ (q : X) (h : Sum.dist (Sum.inr p) (Sum.inl q) = 0), Sum.inr p = Sum.inl q
Tactic: rcases q with q | q
Cleared hypotheses: q, 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
q : X ⊕ Y
p : Y
h : Sum.dist (Sum.inr p) q = 0
inr : ∀ (q : X) (h : Sum.dist (Sum.inr p) (Sum.inl q) = 0), Sum.inr p = Sum.inl q
⊢ Sum.inr p = q
have inr₁ : ∀ (q : Y) (h : Sum.dist.{u, v} (X := X) (Sum.inr p) (Sum.inr q) = 0), Eq (α := X ⊕ Y) (Sum.inr p) (Sum.inr q)
Tactic: rcases q with q | q
Cleared hypotheses: q, 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
p q : X
h : Sum.dist.{u, v} (Y := Y) (Sum.inl p) (Sum.inl q) = 0
⊢ Eq (α := X ⊕ Y) (Sum.inl p) (Sum.inl q)
have inl : Eq (α := X ⊕ Y) (Sum.inl q) (Sum.inl q)
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
p q : Y
h : Sum.dist.{u, v} (X := X) (Sum.inr p) (Sum.inr q) = 0
⊢ Eq (α := X ⊕ Y) (Sum.inr p) (Sum.inr q)
have inr : Eq (α := X ⊕ Y) (Sum.inr q) (Sum.inr q)
Tactic: rw [eq_of_dist_eq_zero h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i = j
⊢ E j = E i
have rw : E j = E j
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (k : ι) ↦ E k) j y)
have rw : 1 ≤ dist x sorry.some + 1 + dist sorry.some y
Tactic: rw [Sigma.dist_ne h x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y
have linarith : dist x sorry.some + 1 + dist sorry.some y < 1 →
  dist x sorry.some + 1 + dist sorry.some y - 1 + (0 - dist x sorry.some) + (0 - dist sorry.some y) = 0
Tactic: linarith [@dist_nonneg _ _ x (Nonempty.some ⟨x⟩), @dist_nonneg _ _ (Nonempty.some ⟨y⟩) y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
x y : (i : ι) × E i
h : dist x y < 1
⊢ x.fst (β := fun (i : ι) ↦ E i) = y.fst (β := fun (i : ι) ↦ E i)
have mk : ∀ (fst : ι) (snd : E fst) (h : dist (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd) y < 1),
  (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd).fst (β := fun (i : ι) ↦ E i) = y.fst (β := fun (i : ι) ↦ E i)
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
y : (i : ι) × E i
fst : ι
snd : E fst
h : dist (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd) y < 1
⊢ (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd).fst (β := fun (i : ι) ↦ E i) = y.fst (β := fun (i : ι) ↦ E i)
have mk : ∀ (fst_1 : ι) (snd_1 : E fst_1)
  (h : dist (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd) (Sigma.mk (β := fun (i : ι) ↦ E i) fst_1 snd_1) < 1),
  (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd).fst (β := fun (i : ι) ↦ E i) =
    (Sigma.mk (β := fun (i : ι) ↦ E i) fst_1 snd_1).fst (β := fun (i : ι) ↦ E i)
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
fst : ι
snd : E fst
fst_1 : ι
snd_1 : E fst_1
h : dist (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd) (Sigma.mk (β := fun (i : ι) ↦ E i) fst_1 snd_1) < 1
⊢ (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd).fst (β := fun (i : ι) ↦ E i) =
    (Sigma.mk (β := fun (i : ι) ↦ E i) fst_1 snd_1).fst (β := fun (i : ι) ↦ E i)
have mk : ∀
  (h :
    (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd).fst (β := fun (i : ι) ↦ E i) ≠
      (Sigma.mk (β := fun (i : ι) ↦ E i) fst_1 snd_1).fst (β := fun (i : ι) ↦ E i)),
  1 ≤ dist (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd) (Sigma.mk (β := fun (i : ι) ↦ E i) fst_1 snd_1)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
x y z : (i : ι) × E i
⊢ dist x z ≤ dist x y + dist y z
have rcases : ∀ (i : ι) (x : E i),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) z ≤ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y + dist y z
Tactic: rcases x with ⟨i, x⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
y z : (i : ι) × E i
i : ι
x : E i
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) z ≤ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y + dist y z
have rcases : ∀ (j : ι) (y : E j),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) z ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) z
Tactic: rcases y with ⟨j, y⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
z : (i : ι) × E i
i : ι
x : E i
j : ι
y : E j
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) z ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) z
have rcases : ∀ (k : ι) (z : E k),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
Tactic: rcases z with ⟨k, z⟩
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inl : ∀ (z : E i),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
Tactic: rcases eq_or_ne i k with (rfl | hik)
Cleared hypotheses: k, z
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
k : ι
z : E k
inl :
  ∀ (z : E i),
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
        dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
have inr : ∀ (hik : i ≠ k),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) k z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
Tactic: rcases eq_or_ne i k with (rfl | hik)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
have inl : ∀ (y : E i),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
Tactic: rcases eq_or_ne i j with (rfl | hij)
Cleared hypotheses: j, y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
inl :
  ∀ (y : E i),
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i y) +
        dist (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
have inl₁ : ∀ (hij : i ≠ j),
  dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
Tactic: rcases eq_or_ne i j with (rfl | hij)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
hij : i ≠ j
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) i z) ≤
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) j y) (Sigma.mk (β := fun (i : ι) ↦ E i) i z)
have inl : dist x z ≤ dist x sorry.some + 1 + dist sorry.some y + (dist y sorry.some + 1 + dist sorry.some z)
Tactic: simp only [Sigma.dist_same, Sigma.dist_ne hij, Sigma.dist_ne hij.symm]