-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : List α} (h : ∀ a ∈ l, p a) (n : Nat) :
    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H)

Proof state:
case cons.succ.h_1.h_2
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁴ : Option α
x✝³ : ∀ (a : α), a ∈ x✝⁴ → p a
x✝² : ∀ (a : α), a ∈ none → p a
h₁ : tl[n✝]? = none
heq✝¹ : HEq ⋯ x✝²
x✝¹ : Option α
x✝ : ∀ (a : α), a ∈ x✝¹ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
h₂ : (hd :: tl)[n✝ + 1]? = some a✝
heq✝ : HEq ⋯ H✝
⊢ none = some (f a✝ ⋯)

Tactic:
simp at h₂

Result:
case cons.succ.h_1.h_2
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁴ : Option α
x✝³ : ∀ (a : α), a ∈ x✝⁴ → p a
x✝² : ∀ (a : α), a ∈ none → p a
h₁ : tl[n✝]? = none
heq✝¹ : HEq ⋯ x✝²
x✝¹ : Option α
x✝ : ∀ (a : α), a ∈ x✝¹ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
heq✝ : HEq ⋯ H✝
h₂ : tl[n✝]? = some a✝
⊢ none = some (f a✝ ⋯)

Proof state:
case cons.succ.h_2.h_1
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁴ : Option α
x✝³ : ∀ (a : α), a ∈ x✝⁴ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
h₁ : tl[n✝]? = some a✝
heq✝¹ : HEq ⋯ H✝
x✝² : Option α
x✝¹ : ∀ (a : α), a ∈ x✝² → p a
x✝ : ∀ (a : α), a ∈ none → p a
h₂ : (hd :: tl)[n✝ + 1]? = none
heq✝ : HEq ⋯ x✝
⊢ some (f a✝ ⋯) = none

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.succ.h_2.h_2
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝³ : Option α
x✝² : ∀ (a : α), a ∈ x✝³ → p a
a✝¹ : α
H✝¹ : ∀ (a : α), a ∈ some a✝¹ → p a
h₁ : tl[n✝]? = some a✝¹
heq✝¹ : HEq ⋯ H✝¹
x✝¹ : Option α
x✝ : ∀ (a : α), a ∈ x✝¹ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
h₂ : (hd :: tl)[n✝ + 1]? = some a✝
heq✝ : HEq ⋯ H✝
⊢ some (f a✝¹ ⋯) = some (f a✝ ⋯)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
⊢ (pmap f (hd :: tl) h)[0]? =
    match (hd :: tl)[0]?, ⋯ with
    | none, x => none
    | some a, H => some (f a ⋯)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons.succ.h_1.h_2
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁴ : Option α
x✝³ : ∀ (a : α), a ∈ x✝⁴ → p a
x✝² : ∀ (a : α), a ∈ none → p a
h₁ : tl[n✝]? = none
heq✝¹ : HEq ⋯ x✝²
x✝¹ : Option α
x✝ : ∀ (a : α), a ∈ x✝¹ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
heq✝ : HEq ⋯ H✝
h₂ : tl[n✝]? = some a✝
⊢ none = some (f a✝ ⋯)

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
n : Nat
⊢ (pmap f [] h)[n]? = Option.pmap f [][n]? ⋯

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.h_1.h_1
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁵ : Option α
x✝⁴ : ∀ (a : α), a ∈ x✝⁵ → p a
x✝³ : ∀ (a : α), a ∈ none → p a
h₁ : tl[n✝]? = none
heq✝¹ : HEq ⋯ x✝³
x✝² : Option α
x✝¹ : ∀ (a : α), a ∈ x✝² → p a
x✝ : ∀ (a : α), a ∈ none → p a
h₂ : (hd :: tl)[n✝ + 1]? = none
heq✝ : HEq ⋯ x✝
⊢ none = none

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
⊢ (match tl[n✝]?, ⋯ with
    | none, x => none
    | some a, H => some (f a ⋯)) =
    match (hd :: tl)[n✝ + 1]?, ⋯ with
    | none, x => none
    | some a, H => some (f a ⋯)

Tactic:
split <;> rename_i h₁ _ <;> split <;> rename_i h₂ _

Result:
case cons.succ.h_1.h_1
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁵ : Option α
x✝⁴ : ∀ (a : α), a ∈ x✝⁵ → p a
x✝³ : ∀ (a : α), a ∈ none → p a
h₁ : tl[n✝]? = none
heq✝¹ : HEq ⋯ x✝³
x✝² : Option α
x✝¹ : ∀ (a : α), a ∈ x✝² → p a
x✝ : ∀ (a : α), a ∈ none → p a
h₂ : (hd :: tl)[n✝ + 1]? = none
heq✝ : HEq ⋯ x✝
⊢ none = none

case cons.succ.h_1.h_2
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁴ : Option α
x✝³ : ∀ (a : α), a ∈ x✝⁴ → p a
x✝² : ∀ (a : α), a ∈ none → p a
h₁ : tl[n✝]? = none
heq✝¹ : HEq ⋯ x✝²
x✝¹ : Option α
x✝ : ∀ (a : α), a ∈ x✝¹ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
h₂ : (hd :: tl)[n✝ + 1]? = some a✝
heq✝ : HEq ⋯ H✝
⊢ none = some (f a✝ ⋯)

case cons.succ.h_2.h_1
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝⁴ : Option α
x✝³ : ∀ (a : α), a ∈ x✝⁴ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
h₁ : tl[n✝]? = some a✝
heq✝¹ : HEq ⋯ H✝
x✝² : Option α
x✝¹ : ∀ (a : α), a ∈ x✝² → p a
x✝ : ∀ (a : α), a ∈ none → p a
h₂ : (hd :: tl)[n✝ + 1]? = none
heq✝ : HEq ⋯ x✝
⊢ some (f a✝ ⋯) = none

case cons.succ.h_2.h_2
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
n✝ : Nat
x✝³ : Option α
x✝² : ∀ (a : α), a ∈ x✝³ → p a
a✝¹ : α
H✝¹ : ∀ (a : α), a ∈ some a✝¹ → p a
h₁ : tl[n✝]? = some a✝¹
heq✝¹ : HEq ⋯ H✝¹
x✝¹ : Option α
x✝ : ∀ (a : α), a ∈ x✝¹ → p a
a✝ : α
H✝ : ∀ (a : α), a ∈ some a✝ → p a
h₂ : (hd :: tl)[n✝ + 1]? = some a✝
heq✝ : HEq ⋯ H✝
⊢ some (f a✝¹ ⋯) = some (f a✝ ⋯)

Proof state:
case cons.zero
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
⊢ (pmap f (hd :: tl) h)[0]? = Option.pmap f (hd :: tl)[0]? ⋯

Tactic:
simp only [Option.pmap]

Result:
case cons.zero
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
hd : α
tl : List α
hl : ∀ (h : ∀ (a : α), a ∈ tl → p a) (n : Nat), (pmap f tl h)[n]? = Option.pmap f tl[n]? ⋯
h : ∀ (a : α), a ∈ hd :: tl → p a
⊢ (pmap f (hd :: tl) h)[0]? =
    match (hd :: tl)[0]?, ⋯ with
    | none, x => none
    | some a, H => some (f a ⋯)