case pos
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a

case neg
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
by_cases h : a ≤ b
case pos.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b
case pos
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
left
no goals
case pos.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ min a b = a ∧ a ≤ b
exact ⟨min_eq_left h, h⟩
case neg.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = b ∧ b < a
case neg
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a
right
no goals
case neg.h
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a✝ b✝ c d a b : α
h : ¬a ≤ b
⊢ min a b = b ∧ b < a
exact ⟨min_eq_right (le_of_lt (not_le.mp h)), not_le.mp h⟩