Theorem: List.length_pmap (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
h : ∀ (a : α), a ∈ l → p a
⊢ length (pmap f l h) = length l
Tactic:
induction l with
| nil => rfl
| cons a l IH => dsimp [pmap]; rw [IH]
State after:
no goals

State before:
case nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
h : ∀ (a : α), a ∈ [] → p a
⊢ length (pmap f [] h) = length []
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ (h : ∀ (a : α), a ∈ l → p a), length (pmap f l h) = length l
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ length (pmap f (a :: l) h) = length (a :: l)
Tactic:
dsimp [pmap]
State after:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ (h : ∀ (a : α), a ∈ l → p a), length (pmap f l h) = length l
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ Nat.succ (length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) = Nat.succ (length l)

State before:
case cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
l : List α
IH : ∀ (h : ∀ (a : α), a ∈ l → p a), length (pmap f l h) = length l
h : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ Nat.succ (length (pmap f l (_ : ∀ (x : α), x ∈ l → p x))) = Nat.succ (length l)
Tactic:
rw [IH]
State after:
no goals