Simplify the LE boilerplate a bit more

Changes

1 changed files (+2/-2)

• Sort.lean
  • @@ -78,12 +78,12 @@ theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort.{0} A).Perm A
    -- Not sure why this needs so much boilerplate @[reducible] - def le (a : (ℕ × String)) (b : (ℕ × String)) := a.1 > b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) + def le (a b : (ℕ × String)) := a.1 > b.1 ∨ (a.1 = b.1 ∧ a.2 ≤ b.2) instance : LE (ℕ × String) where le := le @[grind] - lemma le_def {a : (ℕ × String)} {b : (ℕ × String)} : a ≤ b ↔ le a b := .rfl + lemma le_def {a b : (ℕ × String)} : a ≤ b ↔ le a b := .rfl instance : LinearOrder (ℕ × String) where le_refl := by grind