-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_union {t : Set α} (xs : x ∈ s) (yt : y ∈ t) :
    diam (s ∪ t) ≤ diam s + edist x y + diam t

Proof state:
case inl.inr
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Tactic:
exact A a h'a b h'b

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Tactic:
have Z := A b h'b a h'a

Result:
case inr.inl
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Proof state:
case inr.inl
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Tactic:
rwa [edist_comm] at Z

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t

Tactic:
refine diam_le fun a ha b hb => ?_

Result:
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Proof state:
case inl.inl
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Tactic:
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

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Tactic:
rcases (mem_union _ _ _).1 ha with h'a | h'a <;> rcases (mem_union _ _ _).1 hb with h'b | h'b

Result:
case inl.inl
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Proof state:
case inr.inr
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ 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

Tactic:
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

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t

Tactic:
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)

Result:
α : Type u_1
s : Set α
x y : α
inst✝ : PseudoEMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ diam s + edist x y + diam t
⊢ diam (s ∪ t) ≤ diam s + edist x y + diam t