ι : Type ?u.133209
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
h : map f l = []
⊢ length [] = 0
ι : Type ?u.133209
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
h : map f l = []
⊢ length l = 0
rw [← length_map l f, h]
no goals
ι : Type ?u.133209
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
l : List α
h : map f l = []
⊢ length [] = 0
rfl