awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : Y
q : X
h : Sum.dist (Sum.inr p) (Sum.inl q) = 0
⊢ Sum.inr p = Sum.inl q

Tactic:
eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist q p).symm.trans h)

Premises used: Metric.Sum.dist_eq_glueDist, _private.0.Metric.eq_of_glueDist_eq_zero, Eq.symm, one_pos, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : Y
q : X
h : Sum.dist (Sum.inr p) (Sum.inl q) = 0
⊢ Sum.inr p = Sum.inl q

Tactic:
exact eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist q p).symm.trans h)

Premises used: Metric.Sum.dist_eq_glueDist, _private.0.Metric.eq_of_glueDist_eq_zero, Eq.symm, one_pos, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
inr inr₁ : Eq (α := X ⊕ Y) (Sum.inr q) (Sum.inr q)
⊢ Eq (α := X ⊕ Y) (Sum.inr p) (Sum.inr q)

Tactic:
rw [eq_of_dist_eq_zero h]

Premises used: eq_of_dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
⊢ dist x y = Sum.dist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
⊢ Isometry (α := X) (β := X ⊕ Y) Sum.inl

Tactic:
Isometry.of_dist_eq fun _ _ => rfl

Premises used: Isometry.of_dist_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
⊢ Isometry (α := Y) (β := X ⊕ Y) Sum.inr

Tactic:
Isometry.of_dist_eq fun _ _ => rfl

Premises used: Isometry.of_dist_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i = j
rw rw₁ : E j = E j
⊢ E j = E i

Tactic:
rw [h]
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ dist (Sigma.mk (β := E) i x) (Sigma.mk (β := E) i y) = dist x y

Tactic:
simp [Dist.dist, Sigma.dist]

Premises used: Metric.Sigma.dist, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
⊢ dist (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (k : ι) ↦ E k) j y) =
    dist x ⋯.some + 1 + dist ⋯.some y

Tactic:
dif_neg h

Premises used: dif_neg, dite, Metric.Sigma.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
rw : 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y
⊢ 1 ≤ dist (Sigma.mk (β := fun (k : ι) ↦ E k) i x) (Sigma.mk (β := fun (k : ι) ↦ E k) j y)

Tactic:
rw [Sigma.dist_ne h x y]

Premises used: Metric.Sigma.dist_ne
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i j : ι
h : i ≠ j
x : E i
y : E j
linarith :
  dist x ⋯.some + 1 + dist ⋯.some y < 1 →
    dist x ⋯.some + 1 + dist ⋯.some y - 1 + (0 - dist x ⋯.some) + (0 - dist ⋯.some y) = 0
⊢ 1 ≤ dist x ⋯.some + 1 + dist ⋯.some y

Tactic:
linarith [@dist_nonneg _ _ x (Nonempty.some ⟨x⟩), @dist_nonneg _ _ (Nonempty.some ⟨y⟩) y]

Premises used: dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
x y : (i : ι) × E i
h : dist x y < 1
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)
⊢ x.fst (β := fun (i : ι) ↦ E i) = y.fst (β := fun (i : ι) ↦ E i)

Tactic:
cases x
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
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)
⊢ (Sigma.mk (β := fun (i : ι) ↦ E i) fst snd).fst (β := fun (i : ι) ↦ E i) = y.fst (β := fun (i : ι) ↦ E i)

Tactic:
cases y
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
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)
⊢ (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:
contrapose! h
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 :
  (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:
apply one_le_dist_of_ne h

Premises used: Metric.Sigma.one_le_dist_of_ne
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
x y z : (i : ι) × E i
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
⊢ dist x z ≤ dist x y + dist y z

Tactic:
rcases x with ⟨i, x⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
y z : (i : ι) × E i
i : ι
x : E i
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
⊢ 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 y with ⟨j, y⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
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)
⊢ 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 z with ⟨k, z⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
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)
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
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)
⊢ 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)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x z 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:
simpa using dist_triangle x y z

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
inl : dist x z ≤ dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some 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)

Tactic:
simp only [Sigma.dist_same, Sigma.dist_ne hij, Sigma.dist_ne hij.symm]

Premises used: Ne.symm, Metric.Sigma.dist_ne, Metric.Sigma.dist_same
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 x z ≤ dist x ⋯.some + 0 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + dist ⋯.some z)

Tactic:
simpa only [zero_add, add_zero] using dist_triangle _ _ _

Premises used: dist_triangle, zero_add, add_zero
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 x ⋯.some + 0 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + dist ⋯.some z) ≤
    dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]

Premises used: le_rfl, add_le_add, dist_nonneg, zero_le_one
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 : Dist.dist x z ≤ Dist.dist x ⋯.some + 0 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist ⋯.some z)
dist₁ :
  Dist.dist x ⋯.some + 0 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist ⋯.some z) ≤
    Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)
⊢ Dist.dist x z ≤ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)

Tactic:
calc
        dist x z ≤ dist x (Nonempty.some ⟨x⟩) + 0 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
          simpa only [zero_add, add_zero] using dist_triangle _ _ _
        _ ≤ _ := by apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]

Premises used: Nonempty.some, Nonempty.intro, HAdd.hAdd, Dist.dist, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
hik : i ≠ k
inr :
  ∀ (y : E i),
    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) i y) +
        dist (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)
inr₁ :
  ∀ (hij : i ≠ j),
    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)
⊢ 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 j with (rfl | hij)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
inr : dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x y + (dist y ⋯.some + 1 + dist ⋯.some 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) i y) +
      dist (Sigma.mk (β := fun (i : ι) ↦ E i) i y) (Sigma.mk (β := fun (i : ι) ↦ E i) k z)

Tactic:
simp only [Sigma.dist_ne hik, Sigma.dist_same]

Premises used: Metric.Sigma.dist_ne, Metric.Sigma.dist_same
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x y + dist y ⋯.some + 1 + dist ⋯.some z

Tactic:
apply_rules [add_le_add, le_rfl, dist_triangle]

Premises used: dist_triangle, le_rfl, add_le_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
⊢ dist x y + dist y ⋯.some + 1 + dist ⋯.some z = dist x y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
abel
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
k : ι
z : E k
hik : i ≠ k
y : E i
dist : Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x y + Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z
dist₁ :
  Dist.dist x y + Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z =
    Dist.dist x y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)
⊢ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)

Tactic:
calc
        dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
            dist x y + dist y (Nonempty.some ⟨y⟩) + 1 + dist (Nonempty.some ⟨z⟩) z := by
          apply_rules [add_le_add, le_rfl, dist_triangle]
        _ = _ := by abel

Premises used: Nonempty.some, Nonempty.intro, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
hik : i ≠ k
hij : i ≠ j
inr :
  ∀ (z : E j) (hik : i ≠ j),
    dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j 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) j z)
inr₁ :
  ∀ (hjk : j ≠ 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)
⊢ 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 j k with (rfl | hjk)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
inr : dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + dist y z
⊢ dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) (Sigma.mk (β := fun (i : ι) ↦ E i) j 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) j z)

Tactic:
simp only [Sigma.dist_ne hij, Sigma.dist_same]

Premises used: Metric.Sigma.dist_ne, Metric.Sigma.dist_same
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + (dist ⋯.some y + dist y z)

Tactic:
apply_rules [add_le_add, le_rfl, dist_triangle]

Premises used: dist_triangle, le_rfl, add_le_add
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
⊢ dist x ⋯.some + 1 + (dist ⋯.some y + dist y z) = dist x ⋯.some + 1 + dist ⋯.some y + dist y z

Tactic:
abel
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
z : E j
hik : i ≠ j
dist : Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x ⋯.some + 1 + (Dist.dist ⋯.some y + Dist.dist y z)
dist₁ :
  Dist.dist x ⋯.some + 1 + (Dist.dist ⋯.some y + Dist.dist y z) =
    Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + Dist.dist y z
⊢ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + Dist.dist y z

Tactic:
calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z ≤
              dist x (Nonempty.some ⟨x⟩) + 1 + (dist (Nonempty.some ⟨z⟩) y + dist y z) := by
            apply_rules [add_le_add, le_rfl, dist_triangle]
          _ = _ := by abel

Premises used: Nonempty.some, Nonempty.intro, HAdd.hAdd, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
inr : dist x ⋯.some + 1 + dist ⋯.some z ≤ dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some 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)

Tactic:
simp only [hik, hij, hjk, Sigma.dist_ne, Ne, not_false_iff]

Premises used: Ne, not_false_iff, Metric.Sigma.dist_ne
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x ⋯.some + 1 + dist ⋯.some z = dist x ⋯.some + 1 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + dist ⋯.some z)

Tactic:
simp only [add_zero, zero_add]

Premises used: zero_add, add_zero
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
⊢ dist x ⋯.some + 1 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + dist ⋯.some z) ≤
    dist x ⋯.some + 1 + dist ⋯.some y + (dist y ⋯.some + 1 + dist ⋯.some z)

Tactic:
apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]

Premises used: le_rfl, add_le_add, dist_nonneg, zero_le_one
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
hik : i ≠ k
hij : i ≠ j
hjk : j ≠ k
dist :
  Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z =
    Dist.dist x ⋯.some + 1 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist ⋯.some z)
dist₁ :
  Dist.dist x ⋯.some + 1 + 0 + (HAdd.hAdd (α := ℝ) 0 0 + Dist.dist ⋯.some z) ≤
    Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)
⊢ Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some z ≤
    Dist.dist x ⋯.some + 1 + Dist.dist ⋯.some y + (Dist.dist y ⋯.some + 1 + Dist.dist ⋯.some z)

Tactic:
calc
          dist x (Nonempty.some ⟨x⟩) + 1 + dist (Nonempty.some ⟨z⟩) z =
              dist x (Nonempty.some ⟨x⟩) + 1 + 0 + (0 + 0 + dist (Nonempty.some ⟨z⟩) z) := by
            simp only [add_zero, zero_add]
          _ ≤ _ := by apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]

Premises used: Nonempty.some, Nonempty.intro, HAdd.hAdd, Dist.dist, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
mp : IsOpen[instTopologicalSpaceSigma] s → ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
mpr : (∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen[instTopologicalSpaceSigma] s
⊢ IsOpen[instTopologicalSpaceSigma] s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
⊢ ∃ ε > 0, ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s

Tactic:
Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx

Premises used: Metric.isOpen_iff, Iff.mp, isOpen_sigma_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
mp :
  ∀ (ε : ℝ) (εpos : ε > 0) (hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s),
    ∃ ε > 0, ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < ε → y ∈ s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < ε → y ∈ s

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s :=
      Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx

Premises used: Metric.isOpen_iff, Iff.mp, Sigma.mk, isOpen_sigma_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < ε → y ∈ s

Tactic:
⟨min ε 1, lt_min εpos zero_lt_one, ?_⟩

Premises used: lt_min, zero_lt_one, And.intro, Exists.intro, OfNat.ofNat, Min.min
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
ι : Type u_1
E : ι → Type u_2
inst : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen[instTopologicalSpaceSigma] s
i : ι
x : E i
hx : Sigma.mk (β := fun (i : ι) ↦ E i) i x ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk (β := E) i ⁻¹' s
mp : ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < min ε 1 → y ∈ s
⊢ ∃ ε > 0, ∀ (y : (i : ι) × E i), dist (Sigma.mk (β := fun (i : ι) ↦ E i) i x) y < ε → y ∈ s

Tactic:
refine ⟨min ε 1, lt_min εpos zero_lt_one, ?_⟩