awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
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)
⊢ Sum.dist (Sum.inr val) y = Sum.dist y (Sum.inr val)

Tactic:
cases y
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
val 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:
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm]

Premises used: add_left_comm, dist_comm, add_comm, Metric.Sum.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
val : X
val_1 : Y
⊢ Sum.dist (Sum.inl val) (Sum.inr val_1) = Sum.dist (Sum.inr val_1) (Sum.inl val)

Tactic:
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm]

Premises used: add_left_comm, dist_comm, add_comm, Metric.Sum.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
val : Y
val_1 : X
⊢ Sum.dist (Sum.inr val) (Sum.inl val_1) = Sum.dist (Sum.inl val_1) (Sum.inr val)

Tactic:
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm]

Premises used: add_left_comm, dist_comm, add_comm, Metric.Sum.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
val 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:
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm]

Premises used: add_left_comm, dist_comm, add_comm, Metric.Sum.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
grw₂ grw₃ : LE.le (α := ℝ) 1 1
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)

Tactic:
grw [Sum.dist, ← le_add_of_nonneg_right dist_nonneg, ← le_add_of_nonneg_left dist_nonneg]

Premises used: dist_nonneg, le_add_of_nonneg_right, Metric.Sum.dist, le_add_of_nonneg_left
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y : Y
rw : 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
⊢ 1 ≤ Sum.dist (Sum.inr y) (Sum.inl x)

Tactic:
rw [Sum.dist_comm]

Premises used: _private.0.Metric.Sum.dist_comm
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)

Tactic:
Sum.one_le_dist_inl_inr

Premises used: Metric.Sum.one_le_dist_inl_inr
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)

Tactic:
exact Sum.one_le_dist_inl_inr

Premises used: Metric.Sum.one_le_dist_inl_inr
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
mpr :
  (∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) →
    Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s ↔
    ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
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
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
rcases mem_uniformity_dist.1 hsX with ⟨εX, εX0, hX⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
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
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
rcases mem_uniformity_dist.1 hsY with ⟨εY, εY0, hY⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Gluing
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

Tactic:
⟨min (min εX εY) 1, lt_min (lt_min εX0 εY0) zero_lt_one, ?_⟩

Premises used: lt_min, zero_lt_one, And.intro, Exists.intro, OfNat.ofNat, Min.min
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
mp : ∀ (a b : X ⊕ Y), Sum.dist a b < min (min εX εY) 1 → (a, b) ∈ s
⊢ ∃ ε > 0, ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s

Tactic:
refine ⟨min (min εX εY) 1, lt_min (lt_min εX0 εY0) zero_lt_one, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
a b : X
h : Sum.dist.{u, v} (Y := Y) (Sum.inl a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inl b) ∈ s

Tactic:
hX (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _)))

Premises used: Set.Mem, setOf, min_le_left, Set.preimage, lt_of_lt_of_le, le_trans
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
a b : X
h : Sum.dist.{u, v} (Y := Y) (Sum.inl a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inl b) ∈ s

Tactic:
exact hX (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _)))

Premises used: min_le_left, lt_of_lt_of_le, le_trans
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
a : X
b : Y
h : Sum.dist (Sum.inl a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inr b) ∈ s

Tactic:
cases not_le_of_gt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inl_inr

Premises used: Metric.Sum.one_le_dist_inl_inr, min_le_right, not_le_of_gt, lt_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
a : Y
b : X
h : Sum.dist (Sum.inr a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inl b) ∈ s

Tactic:
cases not_le_of_gt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inr_inl

Premises used: Metric.Sum.one_le_dist_inr_inl, min_le_right, not_le_of_gt, lt_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
a b : Y
h : Sum.dist.{u, v} (X := X) (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
hY (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _)))

Premises used: Set.Mem, setOf, min_le_left, Set.preimage, min_le_right, lt_of_lt_of_le, le_trans
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
a b : Y
h : Sum.dist.{u, v} (X := X) (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
exact hY (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _)))

Premises used: min_le_left, min_le_right, lt_of_lt_of_le, le_trans
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
mpr₁ :
  Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)) s
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) s

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 :
  ∃ ε > 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)
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : X × X) ↦ (Sum.inl p.1, Sum.inl p.2)) (𝓤 X)) s

Tactic:
rw [Filter.mem_map, mem_uniformity_dist]

Premises used: Metric.mem_uniformity_dist, Filter.mem_map
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 :
  ∃ ε > 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)
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (Filter.map (fun (p : Y × Y) ↦ (Sum.inr p.1, Sum.inr p.2)) (𝓤 Y)) s

Tactic:
rw [Filter.mem_map, mem_uniformity_dist]

Premises used: Metric.mem_uniformity_dist, Filter.mem_map
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
⊢ ∃ ε > 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:
⟨ε, ε0, fun _ _ h => H _ _ h⟩

Premises used: Prod.mk, Sum.inl, Prod.fst, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
⊢ ∃ ε > 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:
exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
⊢ ∃ ε > 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:
⟨ε, ε0, fun _ _ h => H _ _ h⟩

Premises used: Prod.mk, Prod.fst, Sum.inr, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
⊢ ∃ ε > 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:
exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
inr : ∀ (val : Y), Sum.dist.{u, v} (X := X) (Sum.inr val) (Sum.inr val) = 0
⊢ Sum.dist x x = 0

Tactic:
cases x
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
val : X
⊢ Sum.dist.{u, v} (Y := Y) (Sum.inl val) (Sum.inl val) = 0

Tactic:
simp only [Sum.dist, dist_self]

Premises used: dist_self, Metric.Sum.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
val : Y
⊢ Sum.dist.{u, v} (X := X) (Sum.inr val) (Sum.inr val) = 0

Tactic:
simp only [Sum.dist, dist_self]

Premises used: dist_self, Metric.Sum.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : X
q : Y
x : X ⊕ Y
simp :
  glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl p) x ≤
    glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl p) (Sum.inr q) +
      glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr q) x
⊢ Sum.dist (Sum.inl p) x ≤ Sum.dist (Sum.inl p) (Sum.inr q) + Sum.dist (Sum.inr q) x

Tactic:
simp only [Sum.dist_eq_glueDist p q]

Premises used: Metric.Sum.dist_eq_glueDist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : X
q : Y
x : X ⊕ Y
⊢ ∀ (p_1 q_1 : Unit), |dist ⋯.some ⋯.some - dist ⋯.some ⋯.some| ≤ HMul.hMul (α := ℝ) 2 1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : X
q : Y
x : X ⊕ Y
⊢ glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl p) x ≤
    glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl p) (Sum.inr q) +
      glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr q) x

Tactic:
exact glueDist_triangle _ _ _ (by simp) _ _ _

Premises used: _private.0.Metric.glueDist_triangle
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X ⊕ Y
q : X
r : Y
simp :
  glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 x (Sum.inr r) ≤
    glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 x (Sum.inl q) +
      glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl q) (Sum.inr r)
⊢ Sum.dist x (Sum.inr r) ≤ Sum.dist x (Sum.inl q) + Sum.dist (Sum.inl q) (Sum.inr r)

Tactic:
simp only [Sum.dist_eq_glueDist q r]

Premises used: Metric.Sum.dist_eq_glueDist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X ⊕ Y
q : X
r : Y
⊢ ∀ (p q_1 : Unit), |dist ⋯.some ⋯.some - dist ⋯.some ⋯.some| ≤ HMul.hMul (α := ℝ) 2 1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X ⊕ Y
q : X
r : Y
⊢ glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 x (Sum.inr r) ≤
    glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 x (Sum.inl q) +
      glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl q) (Sum.inr r)

Tactic:
exact glueDist_triangle _ _ _ (by simp) _ _ _

Premises used: _private.0.Metric.glueDist_triangle
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : Y
x : X ⊕ Y
r : X
simp :
  glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr p) (Sum.inl r) ≤
    glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr p) x +
      glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 x (Sum.inl r)
⊢ Sum.dist (Sum.inr p) (Sum.inl r) ≤ Sum.dist (Sum.inr p) x + Sum.dist x (Sum.inl r)

Tactic:
simp only [Sum.dist_eq_glueDist r p]

Premises used: Metric.Sum.dist_eq_glueDist
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : Y
x : X ⊕ Y
r : X
⊢ ∀ (p_1 q : Unit), |dist ⋯.some ⋯.some - dist ⋯.some ⋯.some| ≤ HMul.hMul (α := ℝ) 2 1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : Y
x : X ⊕ Y
r : X
⊢ glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr p) (Sum.inl r) ≤
    glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr p) x +
      glueDist (fun (x : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 x (Sum.inl r)

Tactic:
exact glueDist_triangle _ _ _ (by simp) _ _ _

Premises used: _private.0.Metric.glueDist_triangle
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
inr : ∀ (p : Y) (h : Sum.dist (Sum.inr p) q = 0), Sum.inr p = q
⊢ p = q

Tactic:
rcases p with p | p
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
inl₁ : ∀ (q : Y) (h : Sum.dist (Sum.inl p) (Sum.inr q) = 0), Sum.inl p = Sum.inr q
⊢ Sum.inl p = q

Tactic:
rcases q with q | q
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
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)
⊢ Sum.inr p = q

Tactic:
rcases q with q | q
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
inl inl₁ : Eq (α := X ⊕ Y) (Sum.inl q) (Sum.inl q)
⊢ Eq (α := X ⊕ Y) (Sum.inl p) (Sum.inl 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
Z : Type w
inst : MetricSpace X
inst_1 : MetricSpace Y
p : X
q : Y
h : Sum.dist (Sum.inl p) (Sum.inr q) = 0
⊢ Sum.inl p = Sum.inr q

Tactic:
eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist p q).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 : X
q : Y
h : Sum.dist (Sum.inl p) (Sum.inr q) = 0
⊢ Sum.inl p = Sum.inr q

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

Premises used: Metric.Sum.dist_eq_glueDist, _private.0.Metric.eq_of_glueDist_eq_zero, Eq.symm, one_pos, Eq.trans