case nil
α : Type u_1
l : List α
p q : α → Bool
n✝ n : ℕ
⊢ countp.go p [] n = n + countp.go p [] 0

case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0
α : Type u_1
l✝ : List α
p q : α → Bool
n : ℕ
l : List α
⊢ countp.go p l n = n + countp.go p l 0
induction' l with head tail ih generalizing n
no goals
case nil
α : Type u_1
l : List α
p q : α → Bool
n✝ n : ℕ
⊢ countp.go p [] n = n + countp.go p [] 0
rfl
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then countp.go p tail (n + 1) else countp.go p tail n) =
    n + bif p head then countp.go p tail (0 + 1) else countp.go p tail 0
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ countp.go p (head :: tail) n = n + countp.go p (head :: tail) 0
unfold countp.go
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then countp.go p tail (n + 1) else countp.go p tail n) =
    n + bif p head then countp.go p tail (0 + 1) else countp.go p tail 0
rw [ih (n := n + 1), ih (n := n), ih (n := 1)]
case pos
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0

case neg
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : ¬p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
case cons
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
by_cases h : p head
no goals
case pos
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
simp [h, add_assoc]
no goals
case neg
α : Type u_1
l : List α
p q : α → Bool
n✝ : ℕ
head : α
tail : List α
ih : ∀ {n : ℕ}, countp.go p tail n = n + countp.go p tail 0
n : ℕ
h : ¬p head = true
⊢ (bif p head then n + 1 + countp.go p tail 0 else n + countp.go p tail 0) =
    n + bif p head then 1 + countp.go p tail 0 else countp.go p tail 0
simp [h]