rcases this with ⟨lt, rfl⟩
case succ.some
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
i : ℕ
hm : (range n).get? m = some i
this : m < n ∧ m = i
⊢ map f (range (min n m)) ++ [f i] = map f (range (min n (m + 1)))
case succ.some.intro
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
n : ℕ
f : ℕ → α
m : ℕ
ih : take m (map f (range n)) = map f (range (min n m))
lt : m < n
hm : (range n).get? m = some m
⊢ map f (range (min n m)) ++ [f m] = map f (range (min n (m + 1)))