unfold maxOfLe
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ maxOfLe.1 a b = a ∨ maxOfLe.1 a b = b
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ { max := fun x y => if x ≤ y then y else x }.1 a b = a ∨ { max := fun x y => if x ≤ y then y else x }.1 a b = b