case step =>
  intro n (ih : AA.OneOfThree (n < m) (n ≃ m) (n > m))
  show AA.OneOfThree (step n < m) (step n ≃ m) (step n > m)
  match ih with
  | AA.OneOfThree.first (_ : n < m) =>
    have : step n ≤ m := lt_step_le.mp ‹n < m›
    have : step n < m ∨ step n ≃ m := le_split ‹step n ≤ m›
    match ‹step n < m ∨ step n ≃ m› with
    | Or.inl (_ : step n < m) => exact AA.OneOfThree.first ‹step n < m›
    | Or.inr (_ : step n ≃ m) => exact AA.OneOfThree.second ‹step n ≃ m›
  | AA.OneOfThree.second (_ : n ≃ m) =>
    have : m ≃ n := Rel.symm ‹n ≃ m›
    have : m ≤ n := le_from_eqv ‹m ≃ n›
    have : step m ≤ step n := AA.subst₁ ‹m ≤ n›
    have : m < step n := lt_step_le.mpr ‹step m ≤ step n›
    apply AA.OneOfThree.third
    exact ‹m < step n›
  | AA.OneOfThree.third (_ : n > m) =>
    apply AA.OneOfThree.third
    show m < step n
    exact lt_trans ‹m < n› lt_step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m : ℕ
motive : ℕ → Prop := fun n => AA.OneOfThree (n < m) (n ≃ m) (n > m)
⊢ ∀ (m : ℕ), motive m → motive (step m)
no goals