α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t
have A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t := fun a ha b hb =>
  calc
    edist a b ≤ edist a x + edist x y + edist y b := edist_triangle4 _ _ _ _
    _ ≤ diam s + edist x y + diam t :=
      add_le_add (add_le_add (edist_le_diam_of_mem ha xs) le_rfl) (edist_le_diam_of_mem yt hb)
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
⊢ edist a b ≤ diam s + edist x y + diam t
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t
refine' diam_le fun a ha b hb => _
case inl.inl
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ s
h'b : b ∈ s
⊢ edist a b ≤ diam s + edist x y + diam t

case inl.inr
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ s
h'b : b ∈ t
⊢ edist a b ≤ diam s + edist x y + diam t

case inr.inl
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ diam s + edist x y + diam t

case inr.inr
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ diam s + edist x y + diam t
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
⊢ edist a b ≤ diam s + edist x y + diam t
cases' (mem_union _ _ _).1 ha with h'a h'a <;> cases' (mem_union _ _ _).1 hb with h'b h'b
no goals
case inl.inl
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ s
h'b : b ∈ s
⊢ edist a b ≤ diam s + edist x y + diam t
calc
  edist a b ≤ diam s := edist_le_diam_of_mem h'a h'b
  _ ≤ diam s + (edist x y + diam t) := le_self_add
  _ = diam s + edist x y + diam t := (add_assoc _ _ _).symm
no goals
case inl.inr
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ s
h'b : b ∈ t
⊢ edist a b ≤ diam s + edist x y + diam t
exact A a h'a b h'b
case inr.inl
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ s
Z : edist b a ≤ diam s + edist x y + diam t
⊢ edist a b ≤ diam s + edist x y + diam t
case inr.inl
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ diam s + edist x y + diam t
have Z := A b h'b a h'a
no goals
case inr.inl
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ s
Z : edist b a ≤ diam s + edist x y + diam t
⊢ edist a b ≤ diam s + edist x y + diam t
rwa [edist_comm] at Z
no goals
case inr.inr
α : Type u
β : Type v
X : Type ?u.298049
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → edist a b ≤ diam s + edist x y + diam t
a : α
ha : a ∈ s ∪ t
b : α
hb : b ∈ s ∪ t
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ diam s + edist x y + diam t
calc
  edist a b ≤ diam t := edist_le_diam_of_mem h'a h'b
  _ ≤ diam s + edist x y + diam t := le_add_self