Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mp.inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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

pp: case mp.inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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

pp: case mp.inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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

pp: case mp.inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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 hX h.1.1

Goal state after:
case mp.inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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

case mp.inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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

case mp.inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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