ι : Type ?u.131877
α : Type u_1
β : Type ?u.131883
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ Min.min (min hs hsn) (min ht htn) ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t))
ι : Type ?u.131877
α : Type u_1
β : Type ?u.131883
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t)) = Min.min (min hs hsn) (min ht htn)
refine' le_antisymm (le_min (IsWf.min_le_min_of_subset (subset_union_left _ _))
  (IsWf.min_le_min_of_subset (subset_union_right _ _))) _
ι : Type ?u.131877
α : Type u_1
β : Type ?u.131883
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ min hs hsn ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t)) ∨
    min ht htn ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t))
ι : Type ?u.131877
α : Type u_1
β : Type ?u.131883
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ Min.min (min hs hsn) (min ht htn) ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t))
rw [min_le_iff]
no goals
ι : Type ?u.131877
α : Type u_1
β : Type ?u.131883
inst✝ : LinearOrder α
s t : Set α
a : α
hs : IsWf s
hsn : Set.Nonempty s
ht : IsWf t
htn : Set.Nonempty t
⊢ min hs hsn ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t)) ∨
    min ht htn ≤ min (_ : IsWf (s ∪ t)) (_ : Set.Nonempty (s ∪ t))
exact ((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp
  (hs.min_le _) (ht.min_le _)