simp[Nat.min_eq_left this, Nat.min_eq_left (Nat.le_step this)]
case succ.none
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
hm : (range n).get? m = none
this : n ≤ m
⊢ map f (range (min n m)) = map f (range (min n (m + 1)))
no goals