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