[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
[PROOFSTEP]
have : ⨅ q, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0 :=
  by
  have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => add_nonneg dist_nonneg dist_nonneg
  refine' le_antisymm _ (le_ciInf A)
  have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
  rw [this]
  exact ciInf_le ⟨0, forall_range_iff.2 A⟩ p
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
⊢ ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0
[PROOFSTEP]
have A : ∀ q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) := fun _ => add_nonneg dist_nonneg dist_nonneg
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0
[PROOFSTEP]
refine' le_antisymm _ (le_ciInf A)
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ 0
[PROOFSTEP]
have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p) := by simp
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
⊢ 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
[PROOFSTEP]
simp
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ 0
[PROOFSTEP]
rw [this]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
A : ∀ (q : Z), 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)
this : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
⊢ ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) ≤ dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p)
[PROOFSTEP]
exact ciInf_le ⟨0, forall_range_iff.2 A⟩ p
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
p : Z
this : ⨅ (q : Z), dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) = 0
⊢ glueDist Φ Ψ ε (Sum.inl (Φ p)) (Sum.inr (Ψ p)) = ε
[PROOFSTEP]
simp only [glueDist, this, zero_add]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val✝¹ : X
val✝ : Y
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inl val✝¹)) (Sum.swap (Sum.inr val✝)) = glueDist Φ Ψ ε (Sum.inl val✝¹) (Sum.inr val✝)
[PROOFSTEP]
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
Φ : Z → X
Ψ : Z → Y
ε : ℝ
val✝¹ : Y
val✝ : X
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inr val✝¹)) (Sum.swap (Sum.inl val✝)) = glueDist Φ Ψ ε (Sum.inr val✝¹) (Sum.inl val✝)
[PROOFSTEP]
simp only [glueDist, Sum.swap_inl, Sum.swap_inr, dist_comm, add_comm]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)
[PROOFSTEP]
rw [glueDist_comm]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : Y
y : X
⊢ ε ≤ glueDist Φ Ψ ε (Sum.inl y) (Sum.inr x)
[PROOFSTEP]
apply le_glueDist_inl_inr
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inr z)
[PROOFSTEP]
simp only [glueDist]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ (⨅ (p : Z), dist x (Φ p) + dist z (Ψ p)) + ε ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ε + dist y z
[PROOFSTEP]
rw [add_right_comm, add_le_add_iff_right]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
⊢ ⨅ (p : Z), dist x (Φ p) + dist z (Ψ p) ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + dist y z
[PROOFSTEP]
refine le_ciInf_add fun p => ciInf_le_of_le ⟨0, ?_⟩ p ?_
[GOAL]
case refine_1
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ 0 ∈ lowerBounds (range fun p => dist x (Φ p) + dist z (Ψ p))
[PROOFSTEP]
exact forall_range_iff.2 fun _ => add_nonneg dist_nonneg dist_nonneg
[GOAL]
case refine_2
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
x : X
y z : Y
p : Z
⊢ dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + dist y (Ψ p) + dist y z
[PROOFSTEP]
linarith [dist_triangle_left z (Ψ p) y]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)
[PROOFSTEP]
simp_rw [glueDist, add_add_add_comm _ ε, add_assoc]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ (p : Z), dist x (Φ p) + dist y (Ψ p)) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
[PROOFSTEP]
refine le_ciInf_add fun p => ?_
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
[PROOFSTEP]
rw [add_left_comm, add_assoc, ← two_mul]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ (⨅ (p : Z), dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
[PROOFSTEP]
refine le_ciInf_add fun q => ?_
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
[PROOFSTEP]
rw [dist_comm z]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p q : Z
⊢ dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
[PROOFSTEP]
linarith [dist_triangle4 x (Φ p) (Φ q) z, dist_triangle_left (Ψ p) (Ψ q) y, (abs_le.1 (H p q)).2]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : 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.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inl z)
[PROOFSTEP]
simp only [← glueDist_swap Φ]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y z : X
⊢ glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl z)) ≤
    glueDist Ψ Φ ε (Sum.swap (Sum.inr x)) (Sum.swap (Sum.inl y)) +
      glueDist Ψ Φ ε (Sum.swap (Sum.inl y)) (Sum.swap (Sum.inl z))
[PROOFSTEP]
apply glueDist_triangle_inl_inr_inr
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : 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)
[PROOFSTEP]
simpa only [glueDist_comm, add_comm] using glueDist_triangle_inl_inr_inr _ _ _ z y x
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : 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)
[PROOFSTEP]
simpa only [← glueDist_swap Φ, glueDist_comm, add_comm, Sum.swap_inl, Sum.swap_inr] using
  glueDist_triangle_inl_inr_inr Ψ Φ ε z y x
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y : X
z : Y
⊢ glueDist Φ Ψ ε (Sum.inr x) (Sum.inr z) ≤
    glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) + glueDist Φ Ψ ε (Sum.inl y) (Sum.inr z)
[PROOFSTEP]
simp only [← glueDist_swap Φ]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : Y
y : X
z : Y
⊢ 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))
[PROOFSTEP]
apply glueDist_triangle_inl_inr_inl
[GOAL]
case H
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : 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 * ε
[PROOFSTEP]
simpa only [abs_sub_comm]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : X
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) = 0
⊢ Sum.inl x = Sum.inl y
[PROOFSTEP]
rw [eq_of_dist_eq_zero h]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ Sum.inl x = Sum.inr y
[PROOFSTEP]
exfalso
[GOAL]
case h
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : X
y : Y
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) = 0
⊢ False
[PROOFSTEP]
linarith [le_glueDist_inl_inr Φ Ψ ε x y]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ Sum.inr x = Sum.inl y
[PROOFSTEP]
exfalso
[GOAL]
case h
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x : Y
y : X
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y) = 0
⊢ False
[PROOFSTEP]
linarith [le_glueDist_inr_inl Φ Ψ ε x y]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
x y : Y
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inr y) = 0
⊢ Sum.inr x = Sum.inr y
[PROOFSTEP]
rw [eq_of_dist_eq_zero h]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) ↔ ∃ δ, δ > 0 ∧ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
[PROOFSTEP]
simp only [Sum.uniformity, Filter.mem_sup, Filter.mem_map, mem_uniformity_dist, mem_preimage]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε, ε > 0 ∧ ∀ {a b : X}, dist a b < ε → (Sum.inl a, Sum.inl b) ∈ s) ∧
      ∃ ε, ε > 0 ∧ ∀ {a b : Y}, dist a b < ε → (Sum.inr a, Sum.inr b) ∈ s) ↔
    ∃ δ, δ > 0 ∧ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ ((∃ ε, ε > 0 ∧ ∀ {a b : X}, dist a b < ε → (Sum.inl a, Sum.inl b) ∈ s) ∧
      ∃ ε, ε > 0 ∧ ∀ {a b : Y}, dist a b < ε → (Sum.inr a, Sum.inr b) ∈ s) →
    ∃ δ, δ > 0 ∧ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
[PROOFSTEP]
rintro ⟨⟨δX, δX0, hX⟩, δY, δY0, hY⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr b) ∈ s
⊢ ∃ δ, δ > 0 ∧ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s
[PROOFSTEP]
refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr b) ∈ s
⊢ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < min (min δX δY) ε → (a, b) ∈ s
[PROOFSTEP]
rintro (a | a) (b | b) h
[GOAL]
case mp.intro.intro.intro.intro.intro.inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr b) ∈ s
a b : X
h : glueDist Φ Ψ ε (Sum.inl a) (Sum.inl b) < min (min δX δY) ε
⊢ (Sum.inl a, Sum.inl b) ∈ s
[PROOFSTEP]
simp only [lt_min_iff] at h 
[GOAL]
case mp.intro.intro.intro.intro.intro.inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr b) ∈ s
a : X
b : Y
h : glueDist Φ Ψ ε (Sum.inl a) (Sum.inr b) < min (min δX δY) ε
⊢ (Sum.inl a, Sum.inr b) ∈ s
[PROOFSTEP]
simp only [lt_min_iff] at h 
[GOAL]
case mp.intro.intro.intro.intro.intro.inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr b) ∈ s
a : Y
b : X
h : glueDist Φ Ψ ε (Sum.inr a) (Sum.inl b) < min (min δX δY) ε
⊢ (Sum.inr a, Sum.inl b) ∈ s
[PROOFSTEP]
simp only [lt_min_iff] at h 
[GOAL]
case mp.intro.intro.intro.intro.intro.inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr b) ∈ s
a b : Y
h : glueDist Φ Ψ ε (Sum.inr a) (Sum.inr b) < min (min δX δY) ε
⊢ (Sum.inr a, Sum.inr b) ∈ s
[PROOFSTEP]
simp only [lt_min_iff] at h 
[GOAL]
case mp.intro.intro.intro.intro.intro.inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr 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
[PROOFSTEP]
exact hX h.1.1
[GOAL]
case mp.intro.intro.intro.intro.intro.inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr 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
[PROOFSTEP]
exact absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_lt
[GOAL]
case mp.intro.intro.intro.intro.intro.inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr 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
[PROOFSTEP]
exact absurd h.2 (le_glueDist_inr_inl _ _ _ _ _).not_lt
[GOAL]
case mp.intro.intro.intro.intro.intro.inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
δX : ℝ
δX0 : δX > 0
hX : ∀ {a b : X}, dist a b < δX → (Sum.inl a, Sum.inl b) ∈ s
δY : ℝ
δY0 : δY > 0
hY : ∀ {a b : Y}, dist a b < δY → (Sum.inr a, Sum.inr 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
[PROOFSTEP]
exact hY h.1.2
[GOAL]
case mpr
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
inst✝ : Nonempty Z
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ δ, δ > 0 ∧ ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s) →
    (∃ ε, ε > 0 ∧ ∀ {a b : X}, dist a b < ε → (Sum.inl a, Sum.inl b) ∈ s) ∧
      ∃ ε, ε > 0 ∧ ∀ {a b : Y}, dist a b < ε → (Sum.inr a, Sum.inr b) ∈ s
[PROOFSTEP]
rintro ⟨ε, ε0, H⟩
[GOAL]
case mpr.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
hε : 0 < ε✝
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε✝ a b < ε → (a, b) ∈ s
⊢ (∃ ε, ε > 0 ∧ ∀ {a b : X}, dist a b < ε → (Sum.inl a, Sum.inl b) ∈ s) ∧
    ∃ ε, ε > 0 ∧ ∀ {a b : Y}, dist a b < ε → (Sum.inr a, Sum.inr b) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.intro.left
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
hε : 0 < ε✝
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε✝ a b < ε → (a, b) ∈ s
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : X}, dist a b < ε → (Sum.inl a, Sum.inl b) ∈ s
[PROOFSTEP]
exact ⟨ε, ε0, fun h => H _ _ h⟩
[GOAL]
case mpr.intro.intro.right
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
hε : 0 < ε✝
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε✝ a b < ε → (a, b) ∈ s
⊢ ∃ ε, ε > 0 ∧ ∀ {a b : Y}, dist a b < ε → (Sum.inr a, Sum.inr b) ∈ s
[PROOFSTEP]
exact ⟨ε, ε0, fun h => H _ _ h⟩
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Φ✝ : Z → X
Ψ✝ : Z → Y
ε✝ : ℝ
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
ε0 : 0 < ε
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x✝¹ x✝ : X ⊕ Y
⊢ (fun x y => ↑{ val := glueDist Φ Ψ ε x y, property := (_ : 0 ≤ glueDist Φ Ψ ε x y) }) x✝¹ x✝ =
    ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X ⊕ Y
x : X
y : Y
⊢ Sum.dist p q = glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 p q
[PROOFSTEP]
cases p
[GOAL]
case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y : Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) q =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl val✝) q
[PROOFSTEP]
cases q
[GOAL]
case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
x : X
y val✝ : Y
⊢ Sum.dist (Sum.inr val✝) q =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝) q
[PROOFSTEP]
cases q
[GOAL]
case inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl val✝¹)
      (Sum.inl val✝)
[PROOFSTEP]
first
| rfl
| simp [Sum.dist, glueDist, dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl val✝¹)
      (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl val✝¹)
      (Sum.inr val✝)
[PROOFSTEP]
first
| rfl
| simp [Sum.dist, glueDist, dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl val✝¹)
      (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl val✝¹)
      (Sum.inr val✝)
[PROOFSTEP]
simp [Sum.dist, glueDist, dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝¹)
      (Sum.inl val✝)
[PROOFSTEP]
first
| rfl
| simp [Sum.dist, glueDist, dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝¹)
      (Sum.inl val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝¹)
      (Sum.inl val✝)
[PROOFSTEP]
simp [Sum.dist, glueDist, dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝¹)
      (Sum.inr val✝)
[PROOFSTEP]
first
| rfl
| simp [Sum.dist, glueDist, dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) =
    glueDist (fun x_1 => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr val✝¹)
      (Sum.inr val✝)
[PROOFSTEP]
rfl
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x y : X ⊕ Y
⊢ Sum.dist x y = Sum.dist y x
[PROOFSTEP]
cases x
[GOAL]
case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : X
⊢ Sum.dist (Sum.inl val✝) y = Sum.dist y (Sum.inl val✝)
[PROOFSTEP]
cases y
[GOAL]
case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
y : X ⊕ Y
val✝ : Y
⊢ Sum.dist (Sum.inr val✝) y = Sum.dist y (Sum.inr val✝)
[PROOFSTEP]
cases y
[GOAL]
case inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : X
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inl val✝¹)
[PROOFSTEP]
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : X
val✝ : Y
⊢ Sum.dist (Sum.inl val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inl val✝¹)
[PROOFSTEP]
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ : Y
val✝ : X
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inl val✝) = Sum.dist (Sum.inl val✝) (Sum.inr val✝¹)
[PROOFSTEP]
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝¹ val✝ : Y
⊢ Sum.dist (Sum.inr val✝¹) (Sum.inr val✝) = Sum.dist (Sum.inr val✝) (Sum.inr val✝¹)
[PROOFSTEP]
simp [Sum.dist, _root_.dist_comm, add_comm, add_left_comm, add_assoc]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inr y) (Sum.inl x)
[PROOFSTEP]
rw [Sum.dist_comm]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inl x) (Sum.inr y)
[PROOFSTEP]
exact Sum.one_le_dist_inl_inr
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) ↔ ∃ ε, ε > 0 ∧ ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) → ∃ ε, ε > 0 ∧ ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
rintro ⟨hsX, hsY⟩
[GOAL]
case mp.intro
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
⊢ ∃ ε, ε > 0 ∧ ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
rcases mem_uniformity_dist.1 hsX with ⟨εX, εX0, hX⟩
[GOAL]
case mp.intro.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
εX : ℝ
εX0 : εX > 0
hX : ∀ {a b : X}, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
rcases mem_uniformity_dist.1 hsY with ⟨εY, εY0, hY⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
εX : ℝ
εX0 : εX > 0
hX : ∀ {a b : X}, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ {a b : Y}, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.fst, Sum.inr p.snd)) ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
[PROOFSTEP]
refine' ⟨min (min εX εY) 1, lt_min (lt_min εX0 εY0) zero_lt_one, _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
εX : ℝ
εX0 : εX > 0
hX : ∀ {a b : X}, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ {a b : Y}, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.fst, Sum.inr p.snd)) ⁻¹' s
⊢ ∀ (a b : X ⊕ Y), Sum.dist a b < min (min εX εY) 1 → (a, b) ∈ s
[PROOFSTEP]
rintro (a | a) (b | b) h
[GOAL]
case mp.intro.intro.intro.intro.intro.inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
εX : ℝ
εX0 : εX > 0
hX : ∀ {a b : X}, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ {a b : Y}, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.fst, Sum.inr p.snd)) ⁻¹' s
a b : X
h : Sum.dist (Sum.inl a) (Sum.inl b) < min (min εX εY) 1
⊢ (Sum.inl a, Sum.inl b) ∈ s
[PROOFSTEP]
exact hX (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _)))
[GOAL]
case mp.intro.intro.intro.intro.intro.inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
εX : ℝ
εX0 : εX > 0
hX : ∀ {a b : X}, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ {a b : Y}, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.fst, Sum.inr p.snd)) ⁻¹' s
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
[PROOFSTEP]
cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inl_inr
[GOAL]
case mp.intro.intro.intro.intro.intro.inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
εX : ℝ
εX0 : εX > 0
hX : ∀ {a b : X}, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ {a b : Y}, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.fst, Sum.inr p.snd)) ⁻¹' s
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
[PROOFSTEP]
cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) Sum.one_le_dist_inr_inl
[GOAL]
case mp.intro.intro.intro.intro.intro.inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
hsX : s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
hsY : s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
εX : ℝ
εX0 : εX > 0
hX : ∀ {a b : X}, dist a b < εX → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
εY : ℝ
εY0 : εY > 0
hY : ∀ {a b : Y}, dist a b < εY → (a, b) ∈ (fun p => (Sum.inr p.fst, Sum.inr p.snd)) ⁻¹' s
a b : Y
h : Sum.dist (Sum.inr a) (Sum.inr b) < min (min εX εY) 1
⊢ (Sum.inr a, Sum.inr b) ∈ s
[PROOFSTEP]
exact hY (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _)))
[GOAL]
case mpr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ ε, ε > 0 ∧ ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s) → s ∈ 𝓤 (X ⊕ Y)
[PROOFSTEP]
rintro ⟨ε, ε0, H⟩
[GOAL]
case mpr.intro.intro
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ 𝓤 (X ⊕ Y)
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.intro.left
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ (Filter.map (fun p => (Sum.inl p.fst, Sum.inl p.snd)) (𝓤 X)).sets
[PROOFSTEP]
rw [Filter.mem_sets, Filter.mem_map, mem_uniformity_dist]
[GOAL]
case mpr.intro.intro.right
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
s : Set ((X ⊕ Y) × (X ⊕ Y))
ε : ℝ
ε0 : ε > 0
H : ∀ (a b : X ⊕ Y), Sum.dist a b < ε → (a, b) ∈ s
⊢ s ∈ (Filter.map (fun p => (Sum.inr p.fst, Sum.inr p.snd)) (𝓤 Y)).sets
[PROOFSTEP]
rw [Filter.mem_sets, Filter.mem_map, mem_uniformity_dist]
[GOAL]
case mpr.intro.intro.left
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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 < ε → (a, b) ∈ (fun p => (Sum.inl p.fst, Sum.inl p.snd)) ⁻¹' s
[PROOFSTEP]
exact ⟨ε, ε0, fun h => H _ _ h⟩
[GOAL]
case mpr.intro.intro.right
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : 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 < ε → (a, b) ∈ (fun p => (Sum.inr p.fst, Sum.inr p.snd)) ⁻¹' s
[PROOFSTEP]
exact ⟨ε, ε0, fun h => H _ _ h⟩
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X ⊕ Y
⊢ dist x x = 0
[PROOFSTEP]
cases x
[GOAL]
case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝ : X
⊢ dist (Sum.inl val✝) (Sum.inl val✝) = 0
[PROOFSTEP]
simp only [Sum.dist, dist_self]
[GOAL]
case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
val✝ : Y
⊢ dist (Sum.inr val✝) (Sum.inr val✝) = 0
[PROOFSTEP]
simp only [Sum.dist, dist_self]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
x✝ : X ⊕ Y
⊢ dist (Sum.inl p) x✝ ≤ dist (Sum.inl p) (Sum.inr q) + dist (Sum.inr q) x✝
[PROOFSTEP]
simp only [Sum.dist_eq_glueDist p q]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
x✝ : X ⊕ Y
⊢ glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl p) x✝ ≤
    glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl p)
        (Sum.inr q) +
      glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr q) x✝
[PROOFSTEP]
exact glueDist_triangle _ _ _ (by norm_num) _ _ _
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
x✝ : X ⊕ Y
⊢ Unit →
    Unit →
      |dist (Nonempty.some (_ : Nonempty X)) (Nonempty.some (_ : Nonempty X)) -
            dist (Nonempty.some (_ : Nonempty Y)) (Nonempty.some (_ : Nonempty Y))| ≤
        2 * 1
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x✝ : X ⊕ Y
q : X
r : Y
⊢ dist x✝ (Sum.inr r) ≤ dist x✝ (Sum.inl q) + dist (Sum.inl q) (Sum.inr r)
[PROOFSTEP]
simp only [Sum.dist_eq_glueDist q r]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x✝ : X ⊕ Y
q : X
r : Y
⊢ glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 x✝ (Sum.inr r) ≤
    glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 x✝ (Sum.inl q) +
      glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inl q)
        (Sum.inr r)
[PROOFSTEP]
exact glueDist_triangle _ _ _ (by norm_num) _ _ _
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x✝ : X ⊕ Y
q : X
r : Y
⊢ Unit →
    Unit →
      |dist (Nonempty.some (_ : Nonempty X)) (Nonempty.some (_ : Nonempty X)) -
            dist (Nonempty.some (_ : Nonempty Y)) (Nonempty.some (_ : Nonempty Y))| ≤
        2 * 1
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : Y
x✝ : X ⊕ Y
r : X
⊢ dist (Sum.inr p) (Sum.inl r) ≤ dist (Sum.inr p) x✝ + dist x✝ (Sum.inl r)
[PROOFSTEP]
simp only [Sum.dist_eq_glueDist r p]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : Y
x✝ : X ⊕ Y
r : X
⊢ glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr p)
      (Sum.inl r) ≤
    glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 (Sum.inr p) x✝ +
      glueDist (fun x => Nonempty.some (_ : Nonempty X)) (fun x => Nonempty.some (_ : Nonempty Y)) 1 x✝ (Sum.inl r)
[PROOFSTEP]
exact glueDist_triangle _ _ _ (by norm_num) _ _ _
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : Y
x✝ : X ⊕ Y
r : X
⊢ Unit →
    Unit →
      |dist (Nonempty.some (_ : Nonempty X)) (Nonempty.some (_ : Nonempty X)) -
            dist (Nonempty.some (_ : Nonempty Y)) (Nonempty.some (_ : Nonempty Y))| ≤
        2 * 1
[PROOFSTEP]
norm_num
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x✝¹ x✝ : X ⊕ Y
⊢ (fun x y => ↑{ val := Sum.dist x y, property := (_ : 0 ≤ Sum.dist x y) }) x✝¹ x✝ = ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X ⊕ Y
h : dist p q = 0
⊢ p = q
[PROOFSTEP]
cases' p with p p
[GOAL]
case inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : X
h : dist (Sum.inl p) q = 0
⊢ Sum.inl p = q
[PROOFSTEP]
cases' q with q q
[GOAL]
case inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
q : X ⊕ Y
p : Y
h : dist (Sum.inr p) q = 0
⊢ Sum.inr p = q
[PROOFSTEP]
cases' q with q q
[GOAL]
case inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X
h : dist (Sum.inl p) (Sum.inl q) = 0
⊢ Sum.inl p = Sum.inl q
[PROOFSTEP]
rw [eq_of_dist_eq_zero h]
[GOAL]
case inl.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : X
q : Y
h : dist (Sum.inl p) (Sum.inr q) = 0
⊢ Sum.inl p = Sum.inr q
[PROOFSTEP]
exact eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist p q).symm.trans h)
[GOAL]
case inr.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p : Y
q : X
h : dist (Sum.inr p) (Sum.inl q) = 0
⊢ Sum.inr p = Sum.inl q
[PROOFSTEP]
exact eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist q p).symm.trans h)
[GOAL]
case inr.inr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : Y
h : dist (Sum.inr p) (Sum.inr q) = 0
⊢ Sum.inr p = Sum.inr q
[PROOFSTEP]
rw [eq_of_dist_eq_zero h]
[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
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := y } = dist x y
[PROOFSTEP]
simp [Dist.dist, Sigma.dist]
[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 { fst := i, snd := x } { fst := j, snd := y }
[PROOFSTEP]
rw [Sigma.dist_ne h x y]
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y
[PROOFSTEP]
linarith [@dist_nonneg _ _ x (Nonempty.some ⟨x⟩), @dist_nonneg _ _ (Nonempty.some ⟨y⟩) y]
[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 = y.fst
[PROOFSTEP]
cases x
[GOAL]
case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y : (i : ι) × E i
fst✝ : ι
snd✝ : E fst✝
h : dist { fst := fst✝, snd := snd✝ } y < 1
⊢ { fst := fst✝, snd := snd✝ }.fst = y.fst
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : dist { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ } < 1
⊢ { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
[PROOFSTEP]
contrapose! h
[GOAL]
case mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
fst✝¹ : ι
snd✝¹ : E fst✝¹
fst✝ : ι
snd✝ : E fst✝
h : fst✝¹ ≠ fst✝
⊢ 1 ≤ dist { fst := fst✝¹, snd := snd✝¹ } { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
apply one_le_dist_of_ne h
[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
[PROOFSTEP]
rcases x with ⟨i, x⟩
[GOAL]
case mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
y z : (i : ι) × E i
i : ι
x : E i
⊢ dist { fst := i, snd := x } z ≤ dist { fst := i, snd := x } y + dist y z
[PROOFSTEP]
rcases y with ⟨j, y⟩
[GOAL]
case mk.mk
ι : 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 { fst := i, snd := x } z ≤ dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } z
[PROOFSTEP]
rcases z with ⟨k, z⟩
[GOAL]
case mk.mk.mk
ι : 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 { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
[PROOFSTEP]
rcases eq_or_ne i k with (rfl | hik)
[GOAL]
case mk.mk.mk.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
z : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := i, snd := z }
[PROOFSTEP]
rcases eq_or_ne i j with (rfl | hij)
[GOAL]
case mk.mk.mk.inl.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x z y : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := i, snd := y } + dist { fst := i, snd := y } { fst := i, snd := z }
[PROOFSTEP]
simpa using dist_triangle x y z
[GOAL]
case mk.mk.mk.inl.inr
ι : 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 { fst := i, snd := x } { fst := i, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := i, snd := z }
[PROOFSTEP]
simp only [Sigma.dist_same, Sigma.dist_ne hij, Sigma.dist_ne hij.symm]
[GOAL]
case mk.mk.mk.inl.inr
ι : 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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E i))) z)
[PROOFSTEP]
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]
[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 (Nonempty.some (_ : Nonempty (E i))) + 0 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E i))) z)
[PROOFSTEP]
simpa only [zero_add, add_zero] using dist_triangle _ _ _
[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 (Nonempty.some (_ : Nonempty (E i))) + 0 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E i))) z) ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E i))) z)
[PROOFSTEP]
apply_rules [add_le_add, le_rfl, dist_nonneg, zero_le_one]
[GOAL]
case mk.mk.mk.inr
ι : 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
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
[PROOFSTEP]
rcases eq_or_ne i j with (rfl | hij)
[GOAL]
case mk.mk.mk.inr.inl
ι : 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 { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := i, snd := y } + dist { fst := i, snd := y } { fst := k, snd := z }
[PROOFSTEP]
simp only [Sigma.dist_ne hik, Sigma.dist_same]
[GOAL]
case mk.mk.mk.inr.inl
ι : 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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x y + (dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
[PROOFSTEP]
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
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x y + dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z
[PROOFSTEP]
apply_rules [add_le_add, le_rfl, dist_triangle]
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z =
    dist x y + (dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
[PROOFSTEP]
abel
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z =
    dist x y + (dist y (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
[PROOFSTEP]
abel
[GOAL]
case mk.mk.mk.inr.inr
ι : 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
⊢ dist { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
[PROOFSTEP]
rcases eq_or_ne j k with (rfl | hjk)
[GOAL]
case mk.mk.mk.inr.inr.inl
ι : 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 { fst := i, snd := x } { fst := j, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := j, snd := z }
[PROOFSTEP]
simp only [Sigma.dist_ne hij, Sigma.dist_same]
[GOAL]
case mk.mk.mk.inr.inr.inl
ι : 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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z
[PROOFSTEP]
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
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + (dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z)
[PROOFSTEP]
apply_rules [add_le_add, le_rfl, dist_triangle]
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + (dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z) =
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z
[PROOFSTEP]
abel
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + (dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z) =
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y + dist y z
[PROOFSTEP]
abel
[GOAL]
case mk.mk.mk.inr.inr.inr
ι : 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 { fst := i, snd := x } { fst := k, snd := z } ≤
    dist { fst := i, snd := x } { fst := j, snd := y } + dist { fst := j, snd := y } { fst := k, snd := z }
[PROOFSTEP]
simp only [hik, hij, hjk, Sigma.dist_ne, Ne.def, not_false_iff]
[GOAL]
case mk.mk.mk.inr.inr.inr
ι : 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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
[PROOFSTEP]
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]
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z =
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E k))) z)
[PROOFSTEP]
simp only [add_zero, zero_add]
[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 (Nonempty.some (_ : Nonempty (E i))) + 1 + 0 + (0 + 0 + dist (Nonempty.some (_ : Nonempty (E k))) z) ≤
    dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist (Nonempty.some (_ : Nonempty (E j))) y +
      (dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist (Nonempty.some (_ : Nonempty (E k))) z)
[PROOFSTEP]
apply_rules [add_le_add, zero_le_one, dist_nonneg, le_rfl]
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen s ↔ ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ IsOpen s → ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
[PROOFSTEP]
rintro hs ⟨i, x⟩ hx
[GOAL]
case mp.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < ε → y ∈ s
[PROOFSTEP]
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ball x ε ⊆ Sigma.mk i ⁻¹' s := Metric.isOpen_iff.1 (isOpen_sigma_iff.1 hs i) x hx
[GOAL]
case mp.mk.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < ε → y ∈ s
[PROOFSTEP]
refine' ⟨min ε 1, lt_min εpos zero_lt_one, _⟩
[GOAL]
case mp.mk.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
⊢ ∀ (y : (i : ι) × E i), dist { fst := i, snd := x } y < min ε 1 → y ∈ s
[PROOFSTEP]
rintro ⟨j, y⟩ hy
[GOAL]
case mp.mk.intro.intro.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
⊢ { fst := j, snd := y } ∈ s
[PROOFSTEP]
rcases eq_or_ne i j with (rfl | hij)
[GOAL]
case mp.mk.intro.intro.mk.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist { fst := i, snd := x } { fst := i, snd := y } < min ε 1
⊢ { fst := i, snd := y } ∈ s
[PROOFSTEP]
simp only [Sigma.dist_same, lt_min_iff] at hy 
[GOAL]
case mp.mk.intro.intro.mk.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
y : E i
hy : dist x y < ε ∧ dist x y < 1
⊢ { fst := i, snd := y } ∈ s
[PROOFSTEP]
exact hε (mem_ball'.2 hy.1)
[GOAL]
case mp.mk.intro.intro.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
hij : i ≠ j
⊢ { fst := j, snd := y } ∈ s
[PROOFSTEP]
apply (lt_irrefl (1 : ℝ) _).elim
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
hs : IsOpen s
i : ι
x : E i
hx : { fst := i, snd := x } ∈ s
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ Sigma.mk i ⁻¹' s
j : ι
y : E j
hy : dist { fst := i, snd := x } { fst := j, snd := y } < min ε 1
hij : i ≠ j
⊢ 1 < 1
[PROOFSTEP]
calc
  1 ≤ Sigma.dist ⟨i, x⟩ ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
  _ < 1 := hy.trans_le (min_le_right _ _)
[GOAL]
case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
⊢ (∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s) → IsOpen s
[PROOFSTEP]
refine fun H => isOpen_sigma_iff.2 fun i => Metric.isOpen_iff.2 fun x hx => ?_
[GOAL]
case mpr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
⊢ ∃ ε, ε > 0 ∧ ball x ε ⊆ Sigma.mk i ⁻¹' s
[PROOFSTEP]
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, ∀ y, dist (⟨i, x⟩ : Σ j, E j) y < ε → y ∈ s := H ⟨i, x⟩ hx
[GOAL]
case mpr.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
⊢ ∃ ε, ε > 0 ∧ ball x ε ⊆ Sigma.mk i ⁻¹' s
[PROOFSTEP]
refine' ⟨ε, εpos, fun y hy => _⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ y ∈ Sigma.mk i ⁻¹' s
[PROOFSTEP]
apply hε ⟨i, y⟩
[GOAL]
case mpr.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist { fst := i, snd := x } { fst := i, snd := y } < ε
[PROOFSTEP]
rw [Sigma.dist_same]
[GOAL]
case mpr.intro.intro
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
s : Set ((i : ι) × E i)
H : ∀ (x : (i : ι) × E i), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
i : ι
x : E i
hx : x ∈ Sigma.mk i ⁻¹' s
ε : ℝ
εpos : ε > 0
hε : ∀ (y : (j : ι) × E j), dist { fst := i, snd := x } y < ε → y ∈ s
y : E i
hy : y ∈ ball x ε
⊢ dist x y < ε
[PROOFSTEP]
exact mem_ball'.1 hy
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ MetricSpace ((i : ι) × E i)
[PROOFSTEP]
refine' MetricSpace.ofDistTopology Sigma.dist _ _ Sigma.dist_triangle Sigma.isOpen_iff _
[GOAL]
case refine'_1
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ ∀ (x : (i : ι) × E i), Sigma.dist x x = 0
[PROOFSTEP]
rintro ⟨i, x⟩
[GOAL]
case refine'_1.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
⊢ Sigma.dist { fst := i, snd := x } { fst := i, snd := x } = 0
[PROOFSTEP]
simp [Sigma.dist]
[GOAL]
case refine'_2
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ ∀ (x y : (i : ι) × E i), Sigma.dist x y = Sigma.dist y x
[PROOFSTEP]
rintro ⟨i, x⟩ ⟨j, y⟩
[GOAL]
case refine'_2.mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
⊢ Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = Sigma.dist { fst := j, snd := y } { fst := i, snd := x }
[PROOFSTEP]
rcases eq_or_ne i j with (rfl | h)
[GOAL]
case refine'_2.mk.mk.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ Sigma.dist { fst := i, snd := x } { fst := i, snd := y } = Sigma.dist { fst := i, snd := y } { fst := i, snd := x }
[PROOFSTEP]
simp [Sigma.dist, dist_comm]
[GOAL]
case refine'_2.mk.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i ≠ j
⊢ Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = Sigma.dist { fst := j, snd := y } { fst := i, snd := x }
[PROOFSTEP]
simp only [Sigma.dist, dist_comm, h, h.symm, not_false_iff, dif_neg]
[GOAL]
case refine'_2.mk.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i ≠ j
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist y (Nonempty.some (_ : Nonempty (E j))) =
    dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist x (Nonempty.some (_ : Nonempty (E i)))
[PROOFSTEP]
abel
[GOAL]
case refine'_2.mk.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
h : i ≠ j
⊢ dist x (Nonempty.some (_ : Nonempty (E i))) + 1 + dist y (Nonempty.some (_ : Nonempty (E j))) =
    dist y (Nonempty.some (_ : Nonempty (E j))) + 1 + dist x (Nonempty.some (_ : Nonempty (E i)))
[PROOFSTEP]
abel
[GOAL]
case refine'_3
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
⊢ ∀ (x y : (i : ι) × E i), Sigma.dist x y = 0 → x = y
[PROOFSTEP]
rintro ⟨i, x⟩ ⟨j, y⟩
[GOAL]
case refine'_3.mk.mk
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
⊢ Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = 0 → { fst := i, snd := x } = { fst := j, snd := y }
[PROOFSTEP]
rcases eq_or_ne i j with (rfl | hij)
[GOAL]
case refine'_3.mk.mk.inl
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ Sigma.dist { fst := i, snd := x } { fst := i, snd := y } = 0 → { fst := i, snd := x } = { fst := i, snd := y }
[PROOFSTEP]
simp [Sigma.dist]
[GOAL]
case refine'_3.mk.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
⊢ Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = 0 → { fst := i, snd := x } = { fst := j, snd := y }
[PROOFSTEP]
intro h
[GOAL]
case refine'_3.mk.mk.inr
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = 0
⊢ { fst := i, snd := x } = { fst := j, snd := y }
[PROOFSTEP]
apply (lt_irrefl (1 : ℝ) _).elim
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = 0
⊢ 1 < 1
[PROOFSTEP]
calc
  1 ≤ Sigma.dist (⟨i, x⟩ : Σ k, E k) ⟨j, y⟩ := Sigma.one_le_dist_of_ne hij _ _
  _ < 1 := by rw [h]; exact zero_lt_one
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = 0
⊢ Sigma.dist { fst := i, snd := x } { fst := j, snd := y } < 1
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x : E i
j : ι
y : E j
hij : i ≠ j
h : Sigma.dist { fst := i, snd := x } { fst := j, snd := y } = 0
⊢ 0 < 1
[PROOFSTEP]
exact zero_lt_one
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → MetricSpace (E i)
i : ι
x y : E i
⊢ dist { fst := i, snd := x } { fst := i, snd := y } = dist x y
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
⊢ CompleteSpace ((i : ι) × E i)
[PROOFSTEP]
set s : ι → Set (Σ i, E i) := fun i => Sigma.fst ⁻¹' { i }
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
⊢ CompleteSpace ((i : ι) × E i)
[PROOFSTEP]
set U := {p : (Σ k, E k) × Σ k, E k | dist p.1 p.2 < 1}
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
⊢ CompleteSpace ((i : ι) × E i)
[PROOFSTEP]
have hc : ∀ i, IsComplete (s i) := fun i => by
  simp only [← range_sigmaMk]
  exact (isometry_mk i).uniformInducing.isComplete_range
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
i : ι
⊢ IsComplete (s i)
[PROOFSTEP]
simp only [← range_sigmaMk]
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
i : ι
⊢ IsComplete (range (Sigma.mk i))
[PROOFSTEP]
exact (isometry_mk i).uniformInducing.isComplete_range
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
⊢ CompleteSpace ((i : ι) × E i)
[PROOFSTEP]
have hd : ∀ (i j), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j := fun i j x hx y hy hxy =>
  (Eq.symm hx).trans ((fst_eq_of_dist_lt_one _ _ hxy).trans hy)
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ CompleteSpace ((i : ι) × E i)
[PROOFSTEP]
refine' completeSpace_of_isComplete_univ _
[GOAL]
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ IsComplete univ
[PROOFSTEP]
convert isComplete_iUnion_separated hc (dist_mem_uniformity zero_lt_one) hd
[GOAL]
case h.e'_3
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i => Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.fst p.snd < 1}
hc : ∀ (i : ι), IsComplete (s i)
hd : ∀ (i j : ι) (x : (i : ι) × E i), x ∈ s i → ∀ (y : (i : ι) × E i), y ∈ s j → (x, y) ∈ U → i = j
⊢ univ = ⋃ (i : ι), s i
[PROOFSTEP]
simp only [← preimage_iUnion, iUnion_of_singleton, preimage_univ]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
p q : Z
⊢ |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * 0
[PROOFSTEP]
rw [hΦ.dist_eq, hΨ.dist_eq]
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
p q : Z
⊢ |dist p q - dist p q| ≤ 2 * 0
[PROOFSTEP]
simp
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
x✝¹ x✝ : X ⊕ Y
⊢ (fun x y => ↑{ val := glueDist Φ Ψ 0 x y, property := (_ : 0 ≤ glueDist Φ Ψ 0 x y) }) x✝¹ x✝ =
    ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
[PROOFSTEP]
let i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
[PROOFSTEP]
let _ := i.toUniformSpace
[GOAL]
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
⊢ toGlueL hΦ hΨ ∘ Φ = toGlueR hΦ hΨ ∘ Ψ
[PROOFSTEP]
funext
[GOAL]
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ (toGlueL hΦ hΨ ∘ Φ) x✝ = (toGlueR hΦ hΨ ∘ Ψ) x✝
[PROOFSTEP]
simp only [comp, toGlueL, toGlueR]
[GOAL]
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ Quotient.mk'' (Sum.inl (Φ x✝)) = Quotient.mk'' (Sum.inr (Ψ x✝))
[PROOFSTEP]
refine' UniformSpace.SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 _)
[GOAL]
case h
X : Type u
Y : Type v
Z : Type w
inst✝³ : Nonempty Z
inst✝² : MetricSpace Z
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hΦ : Isometry Φ
hΨ : Isometry Ψ
i : PseudoMetricSpace (X ⊕ Y) := gluePremetric hΦ hΨ
x✝¹ : UniformSpace (X ⊕ Y) := PseudoMetricSpace.toUniformSpace
x✝ : Z
⊢ dist (Sum.inl (Φ x✝)) (Sum.inr (Ψ x✝)) = 0
[PROOFSTEP]
exact glueDist_glued_points Φ Ψ 0 _
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
hx : x.fst ≤ 0
hy : y.fst ≤ 0
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
cases' x with i x
[GOAL]
case mk
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
y : (n : ℕ) × X n
hy : y.fst ≤ 0
i : ℕ
x : X i
hx : { fst := i, snd := x }.fst ≤ 0
⊢ inductiveLimitDist f { fst := i, snd := x } y =
    dist (leRecOn hx (fun {k} => f k) { fst := i, snd := x }.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
cases' y with j y
[GOAL]
case mk.mk
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
i : ℕ
x : X i
hx : { fst := i, snd := x }.fst ≤ 0
j : ℕ
y : X j
hy : { fst := j, snd := y }.fst ≤ 0
⊢ inductiveLimitDist f { fst := i, snd := x } { fst := j, snd := y } =
    dist (leRecOn hx (fun {k} => f k) { fst := i, snd := x }.snd)
      (leRecOn hy (fun {k} => f k) { fst := j, snd := y }.snd)
[PROOFSTEP]
obtain rfl : i = 0 := nonpos_iff_eq_zero.1 hx
[GOAL]
case mk.mk
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
j : ℕ
y : X j
hy : { fst := j, snd := y }.fst ≤ 0
x : X 0
hx : { fst := 0, snd := x }.fst ≤ 0
⊢ inductiveLimitDist f { fst := 0, snd := x } { fst := j, snd := y } =
    dist (leRecOn hx (fun {k} => f k) { fst := 0, snd := x }.snd)
      (leRecOn hy (fun {k} => f k) { fst := j, snd := y }.snd)
[PROOFSTEP]
obtain rfl : j = 0 := nonpos_iff_eq_zero.1 hy
[GOAL]
case mk.mk
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x : X 0
hx : { fst := 0, snd := x }.fst ≤ 0
y : X 0
hy : { fst := 0, snd := y }.fst ≤ 0
⊢ inductiveLimitDist f { fst := 0, snd := x } { fst := 0, snd := y } =
    dist (leRecOn hx (fun {k} => f k) { fst := 0, snd := x }.snd)
      (leRecOn hy (fun {k} => f k) { fst := 0, snd := y }.snd)
[PROOFSTEP]
rfl
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
by_cases h : max x.1 y.1 = (m + 1)
[GOAL]
case pos
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : max x.fst y.fst = m + 1
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
generalize m + 1 = m' at *
[GOAL]
case pos
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m m' : ℕ
hx : x.fst ≤ m'
hy : y.fst ≤ m'
h : max x.fst y.fst = m'
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
subst m'
[GOAL]
case pos
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ max x.fst y.fst
hy : y.fst ≤ max x.fst y.fst
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
rfl
[GOAL]
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
have : max x.1 y.1 ≤ succ m := by simp [hx, hy]
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
⊢ max x.fst y.fst ≤ succ m
[PROOFSTEP]
simp [hx, hy]
[GOAL]
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this : max x.fst y.fst ≤ succ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this : max x.fst y.fst ≤ succ m
⊢ max x.fst y.fst ≤ m
[PROOFSTEP]
simpa [h] using of_le_succ this
[GOAL]
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ succ m
this : max x.fst y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
have xm : x.1 ≤ m := le_trans (le_max_left _ _) this
[GOAL]
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ succ m
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
have ym : y.1 ≤ m := le_trans (le_max_right _ _) this
[GOAL]
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ succ m
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd)
[PROOFSTEP]
rw [leRecOn_succ xm, leRecOn_succ ym, (I m).dist_eq]
[GOAL]
case neg
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ
hx : x.fst ≤ m + 1
hy : y.fst ≤ m + 1
h : ¬max x.fst y.fst = m + 1
this✝ : max x.fst y.fst ≤ succ m
this : max x.fst y.fst ≤ m
xm : x.fst ≤ m
ym : y.fst ≤ m
⊢ inductiveLimitDist f x y = dist (leRecOn xm (fun {k} => f k) x.snd) (leRecOn ym (fun {k} => f k) y.snd)
[PROOFSTEP]
exact inductiveLimitDist_eq_dist I x y m xm ym
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x : (n : ℕ) × X n
⊢ dist x x = 0
[PROOFSTEP]
simp [dist, inductiveLimitDist]
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
⊢ dist x y = dist y x
[PROOFSTEP]
let m := max x.1 y.1
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
⊢ dist x y = dist y x
[PROOFSTEP]
have hx : x.1 ≤ m := le_max_left _ _
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
⊢ dist x y = dist y x
[PROOFSTEP]
have hy : y.1 ≤ m := le_max_right _ _
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
⊢ dist x y = dist y x
[PROOFSTEP]
unfold dist
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
⊢ { dist := inductiveLimitDist f }.1 x y = { dist := inductiveLimitDist f }.1 y x
[PROOFSTEP]
simp only
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max x.fst y.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
⊢ inductiveLimitDist f x y = inductiveLimitDist f y x
[PROOFSTEP]
rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y x m hy hx, dist_comm]
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
let m := max (max x.1 y.1) z.1
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
have hx : x.1 ≤ m := le_trans (le_max_left _ _) (le_max_left _ _)
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
hx : x.fst ≤ m
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
have hy : y.1 ≤ m := le_trans (le_max_right _ _) (le_max_left _ _)
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
have hz : z.1 ≤ m := le_max_right _ _
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
hz : z.fst ≤ m
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
calc
  inductiveLimitDist f x z = dist (leRecOn hx (f _) x.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
    inductiveLimitDist_eq_dist I x z m hx hz
  _ ≤
      dist (leRecOn hx (f _) x.2 : X m) (leRecOn hy (f _) y.2 : X m) +
        dist (leRecOn hy (f _) y.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
    (dist_triangle _ _ _)
  _ = inductiveLimitDist f x y + inductiveLimitDist f y z := by
    rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max x.fst y.fst) z.fst
hx : x.fst ≤ m
hy : y.fst ≤ m
hz : z.fst ≤ m
⊢ dist (leRecOn hx (fun {k} => f k) x.snd) (leRecOn hy (fun {k} => f k) y.snd) +
      dist (leRecOn hy (fun {k} => f k) y.snd) (leRecOn hz (fun {k} => f k) z.snd) =
    inductiveLimitDist f x y + inductiveLimitDist f y z
[PROOFSTEP]
rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x✝¹ x✝ : (n : ℕ) × X n
⊢ (fun x y => ↑{ val := inductiveLimitDist f x y, property := (_ : 0 ≤ inductiveLimitDist f x y) }) x✝¹ x✝ =
    ENNReal.ofReal (dist x✝¹ x✝)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ dist (toInductiveLimit I n x) (toInductiveLimit I n y) = dist x y
[PROOFSTEP]
change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ inductiveLimitDist f { fst := n, snd := x } { fst := n, snd := y } = dist x y
[PROOFSTEP]
rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self, leRecOn_self]
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
⊢ toInductiveLimit I (succ n) ∘ f n = toInductiveLimit I n
[PROOFSTEP]
let _ := inductivePremetric I
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
⊢ toInductiveLimit I (succ n) ∘ f n = toInductiveLimit I n
[PROOFSTEP]
funext x
[GOAL]
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ (toInductiveLimit I (succ n) ∘ f n) x = toInductiveLimit I n x
[PROOFSTEP]
simp only [comp, toInductiveLimit]
[GOAL]
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ Quotient.mk'' { fst := succ n, snd := f n x } = Quotient.mk'' { fst := n, snd := x }
[PROOFSTEP]
refine' UniformSpace.SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 _)
[GOAL]
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ dist { fst := succ n, snd := f n x } { fst := n, snd := x } = 0
[PROOFSTEP]
show inductiveLimitDist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0
[GOAL]
case h
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ inductiveLimitDist f { fst := succ n, snd := f n x } { fst := n, snd := x } = 0
[PROOFSTEP]
rw [inductiveLimitDist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, leRecOn_self, leRecOn_succ, leRecOn_self, dist_self]
[GOAL]
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := n, snd := x }.fst ≤ { fst := n, snd := x }.fst
case h.h2
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := n, snd := x }.fst ≤ n + 1
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x✝ : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric I
x : X n
⊢ { fst := succ n, snd := f n x }.fst ≤ { fst := succ n, snd := f n x }.fst
[PROOFSTEP]
exacts [le_rfl, le_succ _, le_rfl]
