case nil
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
l₂ : List α
h : [] <+: l₂
⊢ List.map f [] <+: List.map f l₂

case cons
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
l₂ : List α
h : hd :: tl <+: l₂
⊢ List.map f (hd :: tl) <+: List.map f l₂
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h : l₁ <+: l₂
f : α → β
⊢ List.map f l₁ <+: List.map f l₂
induction' l₁ with hd tl hl generalizing l₂
no goals
case nil
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
l₂ : List α
h : [] <+: l₂
⊢ List.map f [] <+: List.map f l₂
simp only [nil_prefix, map_nil]
case cons.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
h : hd :: tl <+: []
⊢ List.map f (hd :: tl) <+: List.map f []

case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd :: tl <+: hd₂ :: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
case cons
α : Type u_1
β : Type u_2
l l₁ l₂✝ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂✝
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
l₂ : List α
h : hd :: tl <+: l₂
⊢ List.map f (hd :: tl) <+: List.map f l₂
cases' l₂ with hd₂ tl₂
no goals
case cons.nil
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
h : hd :: tl <+: []
⊢ List.map f (hd :: tl) <+: List.map f []
simpa only using eq_nil_of_prefix_nil h
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd = hd₂ ∧ tl <+: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd :: tl <+: hd₂ :: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
rw [cons_prefix_iff] at h
no goals
case cons.cons
α : Type u_1
β : Type u_2
l l₁ l₂ l₃ : List α
a b : α
m n : ℕ
h✝ : l₁ <+: l₂
f : α → β
hd : α
tl : List α
hl : ∀ {l₂ : List α}, tl <+: l₂ → List.map f tl <+: List.map f l₂
hd₂ : α
tl₂ : List α
h : hd = hd₂ ∧ tl <+: tl₂
⊢ List.map f (hd :: tl) <+: List.map f (hd₂ :: tl₂)
simp only [List.map_cons, h, prefix_cons_inj, hl, map]