exact Fin.cases (by simpa using Nat.unpair_left_le _) (fun i => le_trans (ih e.unpair.2 i) (Nat.unpair_right_le _)) i
case succ
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) i ≤ e
no goals