case nil
ι : Type ?u.326072
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : List α
H₁✝ : ∀ (a : α), a ∈ l → p a
H₂✝ : ∀ (a : α), a ∈ l → q a
h✝ : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
H₁ : ∀ (a : α), a ∈ [] → p a
H₂ : ∀ (a : α), a ∈ [] → q a
h : ∀ (a : α), a ∈ [] → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f [] H₁ = pmap g [] H₂

case cons
ι : Type ?u.326072
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : List α
H₁✝ : ∀ (a : α), a ∈ l → p a
H₂✝ : ∀ (a : α), a ∈ l → q a
h✝ : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
head✝ : α
tail✝ : List α
ih :
  ∀ {H₁ : ∀ (a : α), a ∈ tail✝ → p a} {H₂ : ∀ (a : α), a ∈ tail✝ → q a},
    (∀ (a : α), a ∈ tail✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → pmap f tail✝ H₁ = pmap g tail✝ H₂
H₁ : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
H₂ : ∀ (a : α), a ∈ head✝ :: tail✝ → q a
h : ∀ (a : α), a ∈ head✝ :: tail✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f (head✝ :: tail✝) H₁ = pmap g (head✝ :: tail✝) H₂
ι : Type ?u.326072
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : List α
H₁ : ∀ (a : α), a ∈ l → p a
H₂ : ∀ (a : α), a ∈ l → q a
h : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f l H₁ = pmap g l H₂
induction' l with _ _ ih
no goals
case nil
ι : Type ?u.326072
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : List α
H₁✝ : ∀ (a : α), a ∈ l → p a
H₂✝ : ∀ (a : α), a ∈ l → q a
h✝ : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
H₁ : ∀ (a : α), a ∈ [] → p a
H₂ : ∀ (a : α), a ∈ [] → q a
h : ∀ (a : α), a ∈ [] → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f [] H₁ = pmap g [] H₂
rfl
no goals
case cons
ι : Type ?u.326072
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p q : α → Prop
f : (a : α) → p a → β
g : (a : α) → q a → β
l : List α
H₁✝ : ∀ (a : α), a ∈ l → p a
H₂✝ : ∀ (a : α), a ∈ l → q a
h✝ : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
head✝ : α
tail✝ : List α
ih :
  ∀ {H₁ : ∀ (a : α), a ∈ tail✝ → p a} {H₂ : ∀ (a : α), a ∈ tail✝ → q a},
    (∀ (a : α), a ∈ tail✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂) → pmap f tail✝ H₁ = pmap g tail✝ H₂
H₁ : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
H₂ : ∀ (a : α), a ∈ head✝ :: tail✝ → q a
h : ∀ (a : α), a ∈ head✝ :: tail✝ → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂
⊢ pmap f (head✝ :: tail✝) H₁ = pmap g (head✝ :: tail✝) H₂
rw [pmap, pmap, h _ (mem_cons_self _ _), ih fun a ha => h a (mem_cons_of_mem _ ha)]