case nil
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h✝ : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
h : ∀ (a : ι), a ∈ [] ++ l₂ → p a
⊢ pmap f ([] ++ l₂) h = pmap f [] (_ : ∀ (a : ι), a ∈ [] → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)

case cons
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h✝ : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
head✝ : ι
tail✝ : List ι
ih :
  ∀ (h : ∀ (a : ι), a ∈ tail✝ ++ l₂ → p a),
    pmap f (tail✝ ++ l₂) h = pmap f tail✝ (_ : ∀ (a : ι), a ∈ tail✝ → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
h : ∀ (a : ι), a ∈ head✝ :: tail✝ ++ l₂ → p a
⊢ pmap f (head✝ :: tail✝ ++ l₂) h =
    pmap f (head✝ :: tail✝) (_ : ∀ (a : ι), a ∈ head✝ :: tail✝ → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
⊢ pmap f (l₁ ++ l₂) h = pmap f l₁ (_ : ∀ (a : ι), a ∈ l₁ → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
induction' l₁ with _ _ ih
no goals
case nil
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h✝ : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
h : ∀ (a : ι), a ∈ [] ++ l₂ → p a
⊢ pmap f ([] ++ l₂) h = pmap f [] (_ : ∀ (a : ι), a ∈ [] → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
rfl
case cons
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h✝ : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
head✝ : ι
tail✝ : List ι
ih :
  ∀ (h : ∀ (a : ι), a ∈ tail✝ ++ l₂ → p a),
    pmap f (tail✝ ++ l₂) h = pmap f tail✝ (_ : ∀ (a : ι), a ∈ tail✝ → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
h : ∀ (a : ι), a ∈ head✝ :: tail✝ ++ l₂ → p a
⊢ f head✝ (_ : p head✝) :: pmap f (tail✝ ++ l₂) (_ : ∀ (x : ι), x ∈ tail✝ ++ l₂ → p x) =
    f head✝ (_ : p head✝) :: (pmap f tail✝ (_ : ∀ (x : ι), x ∈ tail✝ → p x) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a))
case cons
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h✝ : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
head✝ : ι
tail✝ : List ι
ih :
  ∀ (h : ∀ (a : ι), a ∈ tail✝ ++ l₂ → p a),
    pmap f (tail✝ ++ l₂) h = pmap f tail✝ (_ : ∀ (a : ι), a ∈ tail✝ → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
h : ∀ (a : ι), a ∈ head✝ :: tail✝ ++ l₂ → p a
⊢ pmap f (head✝ :: tail✝ ++ l₂) h =
    pmap f (head✝ :: tail✝) (_ : ∀ (a : ι), a ∈ head✝ :: tail✝ → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
dsimp only [pmap, cons_append]
no goals
case cons
ι : Type u_1
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
p : ι → Prop
f : (a : ι) → p a → α
l₁ l₂ : List ι
h✝ : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a
head✝ : ι
tail✝ : List ι
ih :
  ∀ (h : ∀ (a : ι), a ∈ tail✝ ++ l₂ → p a),
    pmap f (tail✝ ++ l₂) h = pmap f tail✝ (_ : ∀ (a : ι), a ∈ tail✝ → p a) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a)
h : ∀ (a : ι), a ∈ head✝ :: tail✝ ++ l₂ → p a
⊢ f head✝ (_ : p head✝) :: pmap f (tail✝ ++ l₂) (_ : ∀ (x : ι), x ∈ tail✝ ++ l₂ → p x) =
    f head✝ (_ : p head✝) :: (pmap f tail✝ (_ : ∀ (x : ι), x ∈ tail✝ → p x) ++ pmap f l₂ (_ : ∀ (a : ι), a ∈ l₂ → p a))
rw [ih]