ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ min a b = if b ≤ a then b else a
rw [min_def]
case inl
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

case inr.inl
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a

case inr.inr
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
rcases lt_trichotomy a b with (lt | eq | gt)
no goals
case inl
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
lt : a < b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
rw [if_pos lt.le, if_neg (not_le.mpr lt)]
no goals
case inr.inl
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
eq : a = b
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
rw [if_pos eq.le, if_pos eq.ge, eq]
no goals
case inr.inr
ι : Type ?u.6580
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.6591
r : α → α → Prop
inst✝ : LinearOrder α
a b : α
gt : b < a
⊢ (if a ≤ b then a else b) = if b ≤ a then b else a
rw [if_neg (not_le.mpr gt.gt), if_pos gt.le]