no goals
ι : Type ?u.219275
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
i : ℕ
⊢ map f (drop i []) = drop i (map f [])
simp
no goals
ι : Type ?u.219275
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
L : List α
⊢ map f (drop 0 L) = drop 0 (map f L)
simp
ι : Type ?u.219275
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : ℕ
⊢ map f (drop n t) = drop n (map f t)
ι : Type ?u.219275
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : ℕ
⊢ map f (drop (n + 1) (h :: t)) = drop (n + 1) (map f (h :: t))
dsimp
no goals
ι : Type ?u.219275
α✝ : Type u
β✝ : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α✝
α : Type u_1
β : Type u_2
f : α → β
h : α
t : List α
n : ℕ
⊢ map f (drop n t) = drop n (map f t)
rw [map_drop f t]