case inl
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t

case inr
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : Set.Nonempty s
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
cases' s.eq_empty_or_nonempty with hs hs
case inl.inl
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : t = ∅
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t

case inl.inr
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : Set.Nonempty t
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
case inl
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
cases' t.eq_empty_or_nonempty with ht ht
no goals
case inl.inl
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : t = ∅
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
exact Or.inl ⟨hs, ht⟩
case inl.inr
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist t s ≠ ⊤
hs : s = ∅
ht : Set.Nonempty t
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
case inl.inr
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : s = ∅
ht : Set.Nonempty t
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
rw [hausdorffEdist_comm] at fin
no goals
case inl.inr
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist t s ≠ ⊤
hs : s = ∅
ht : Set.Nonempty t
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
exact Or.inr ⟨nonempty_of_hausdorffEdist_ne_top ht fin, ht⟩
no goals
case inr
ι : Sort ?u.55945
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t u : Set α
Φ : α → β
fin : hausdorffEdist s t ≠ ⊤
hs : Set.Nonempty s
⊢ s = ∅ ∧ t = ∅ ∨ Set.Nonempty s ∧ Set.Nonempty t
exact Or.inr ⟨hs, nonempty_of_hausdorffEdist_ne_top hs fin⟩