match le_step_split ‹m ≤ step k› with
| Or.inl (_ : m ≤ k) =>
  exact le_step (ih ‹m ≤ k›)
| Or.inr (_ : m ≃ step k) =>
  exact AA.substRFn ‹m ≃ step k› ‹n ≤ m›
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n m k✝ : ℕ
x✝¹ : n ≤ m
d : ℕ
h✝ : n + d ≃ m
k : ℕ
ih : m ≤ k → n ≤ k
x✝ : m ≤ step k
⊢ n ≤ step k
no goals