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
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.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)

Tactic:
simpa only [glueDist_comm, add_comm] using glueDist_triangle_inl_inr_inr _ _ _ z y x

Premises used: add_comm, _private.0.Metric.glueDist_triangle_inl_inr_inr, _private.0.Metric.glueDist_comm
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 : X
z : Y
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inr z)

Tactic:
simpa only [← glueDist_swap Φ, glueDist_comm, add_comm, Sum.swap_inl, Sum.swap_inr]
      using glueDist_triangle_inl_inr_inr Ψ Φ ε z y x

Premises used: Sum.swap_inr, add_comm, Metric.glueDist_swap, _private.0.Metric.glueDist_triangle_inl_inr_inr, _private.0.Metric.glueDist_comm, Sum.swap_inl
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
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))
⊢ glueDist Φ Ψ ε (Sum.inr x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inr z)

Tactic:
simp only [← glueDist_swap Φ]

Premises used: Metric.glueDist_swap
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
H₁ : ∀ (p q : Z), |dist (Ψ p) (Ψ q) - dist (Φ p) (Φ q)| ≤ 2 * ε
⊢ 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:
apply glueDist_triangle_inl_inr_inl

Premises used: _private.0.Metric.glueDist_triangle_inl_inr_inl
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
⊢ ∀ (p q : Z), |dist (Ψ p) (Ψ q) - dist (Φ p) (Φ q)| ≤ 2 * ε

Tactic:
simpa only [abs_sub_comm]

Premises used: abs_sub_comm
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
rw rw₁ : Eq (α := X ⊕ Y) (Sum.inl y) (Sum.inl y)
⊢ Eq (α := X ⊕ Y) (Sum.inl x) (Sum.inl y)

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
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
exfalso : False
⊢ Sum.inl x = Sum.inr y

Tactic:
exfalso
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
linarith : 0 - ε + (glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) - 0) + (ε - glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y)) = 0
⊢ False

Tactic:
linarith [le_glueDist_inl_inr Φ Ψ ε x y]

Premises used: Metric.le_glueDist_inl_inr
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
exfalso : False
⊢ Sum.inr x = Sum.inl y

Tactic:
exfalso
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
linarith : 0 - ε + (glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) - 0) + (ε - glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)) = 0
⊢ False

Tactic:
linarith [le_glueDist_inr_inl Φ Ψ ε x y]

Premises used: Metric.le_glueDist_inr_inl
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
rw rw₁ : Eq (α := X ⊕ Y) (Sum.inr y) (Sum.inr y)
⊢ Eq (α := X ⊕ Y) (Sum.inr x) (Sum.inr y)

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
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
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
⊢ Membership.mem (γ := Filter ((X ⊕ Y) × (X ⊕ Y))) (𝓤 (X ⊕ Y)) 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]

Premises used: Metric.mem_uniformity_dist, Filter.mem_sup, Sum.uniformity, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
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
⊢ ((∃ ε > 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
-- Module: Mathlib.Topology.MetricSpace.Gluing
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

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

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

Tactic:
refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) ε
⊢ (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

Premises used: lt_min_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) ε
⊢ (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

Premises used: lt_min_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) ε
⊢ (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

Premises used: lt_min_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) ε
⊢ (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

Premises used: lt_min_iff
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < ε
⊢ (Sum.inl a, Sum.inl b) ∈ s

Tactic:
hX h.1.1

Premises used: Set.Mem, Prod.map, And.left
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < ε
⊢ (Sum.inl a, Sum.inl b) ∈ s

Tactic:
exact hX h.1.1

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < ε
⊢ (Sum.inl a, Sum.inr b) ∈ s

Tactic:
absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_gt

Premises used: Metric.le_glueDist_inl_inr, absurd, And.right, LE.le.not_gt
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < ε
⊢ (Sum.inl a, Sum.inr b) ∈ s

Tactic:
exact absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_gt

Premises used: Metric.le_glueDist_inl_inr, absurd, And.right, LE.le.not_gt
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < ε
⊢ (Sum.inr a, Sum.inl b) ∈ s

Tactic:
absurd h.2 (le_glueDist_inr_inl _ _ _ _ _).not_gt

Premises used: Metric.le_glueDist_inr_inl, absurd, And.right, LE.le.not_gt
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < ε
⊢ (Sum.inr a, Sum.inl b) ∈ s

Tactic:
exact absurd h.2 (le_glueDist_inr_inl _ _ _ _ _).not_gt

Premises used: Metric.le_glueDist_inr_inl, absurd, And.right, LE.le.not_gt
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < ε
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
hY h.1.2

Premises used: Set.Mem, Prod.map, And.right, And.left
-- Module: Mathlib.Topology.MetricSpace.Gluing
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) < δX ∧ glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < δY) ∧
    glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < ε
⊢ (Sum.inr a, Sum.inr b) ∈ s

Tactic:
exact hY h.1.2

Premises used: And.right, And.left
-- Module: Mathlib.Topology.MetricSpace.Gluing
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
mpr₁ : ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (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
-- Module: Mathlib.Topology.MetricSpace.Gluing
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

Tactic:
⟨ε, ε0, fun _ _ h => H _ _ h⟩

Premises used: Sum.inl, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Gluing
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

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
Φ : 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 : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s

Tactic:
⟨ε, ε0, fun _ _ h => H _ _ h⟩

Premises used: Sum.inr, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Gluing
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 : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s

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
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
inr :
  ∀ (val : Y),
    Sum.dist (Sum.inr val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) q
⊢ Sum.dist p q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 p q

Tactic:
cases p
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
inl₁ :
  ∀ (val_1 : Y),
    Sum.dist (Sum.inl val) (Sum.inr val_1) =
      glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) (Sum.inr val_1)
⊢ Sum.dist (Sum.inl val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) q

Tactic:
cases q
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
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) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) (Sum.inr val_1)
⊢ Sum.dist (Sum.inr val) q = glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) q

Tactic:
cases q
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y : Y
val 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)

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y : Y
val 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)

Tactic:
first | rfl | simp [Sum.dist, glueDist, dist_comm, add_comm,
    add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc, dist_comm, add_comm, Metric.glueDist, 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
val : X
val_1 : Y
⊢ Sum.dist (Sum.inl val) (Sum.inr val_1) =
    glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) (Sum.inr val_1)

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

Premises used: add_left_comm, add_assoc, dist_comm, add_comm, Metric.glueDist, 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
val : X
val_1 : Y
⊢ Sum.dist (Sum.inl val) (Sum.inr val_1) =
    glueDist (fun (x_1 : Unit) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inl val) (Sum.inr val_1)

Tactic:
first | rfl | simp [Sum.dist, glueDist, dist_comm, add_comm,
    add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc, dist_comm, add_comm, Metric.glueDist, 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 val : Y
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)

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

Premises used: add_left_comm, add_assoc, dist_comm, add_comm, Metric.glueDist, 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 val : Y
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)

Tactic:
first | rfl | simp [Sum.dist, glueDist, dist_comm, add_comm,
    add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc, dist_comm, add_comm, Metric.glueDist, 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 val 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) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) (Sum.inr val_1)

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Gluing
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x : X
y val 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) ↦ ⋯.some) (fun (x : Unit) ↦ ⋯.some) 1 (Sum.inr val) (Sum.inr val_1)

Tactic:
first | rfl | simp [Sum.dist, glueDist, dist_comm, add_comm,
    add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc, dist_comm, add_comm, Metric.glueDist, Metric.Sum.dist
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
inr : ∀ (val : Y), Sum.dist (Sum.inr val) y = Sum.dist y (Sum.inr val)
⊢ Sum.dist x y = Sum.dist y x

Tactic:
cases x
-- Module: Mathlib.Topology.MetricSpace.Gluing
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)
inl₁ : ∀ (val_1 : Y), Sum.dist (Sum.inl val) (Sum.inr val_1) = Sum.dist (Sum.inr val_1) (Sum.inl val)
⊢ Sum.dist (Sum.inl val) y = Sum.dist y (Sum.inl val)

Tactic:
cases y