ι : Type ?u.76194
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.76205
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ (if ¬y ≤ x then x else y) = if x < y then x else y
ι : Type ?u.76194
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.76205
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ min x y = if x < y then x else y
rw [min_comm, min_def, ← ite_not]
no goals
ι : Type ?u.76194
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.76205
r : α → α → Prop
inst✝ : LinearOrder α
p : α → Prop
x✝ y✝ x y : α
⊢ (if ¬y ≤ x then x else y) = if x < y then x else y
simp only [not_le]