case mpr =>
  intro (_ : lt n m)
  show n < m
  have (And.intro (_ : le n m) (_ : n ≄ m)) := ‹lt n m›
  have : n ≤ m := prelude_le_iff_impl_le.mpr ‹le n m›
  have : n = m ∨ n < m := Nat.eq_or_lt_of_le ‹n ≤ m›
  match ‹n = m ∨ n < m› with
  | Or.inl (_ : n = m) =>
    have : n ≠ m := ‹n ≄ m›
    exact absurd ‹n = m› ‹n ≠ m›
  | Or.inr (_ : n < m) =>
    exact ‹n < m›
n m : Nat
⊢ lt n m → n < m
no goals