case nil
α : Type u_1
l : List α
p q : α → Bool
⊢ length [] = countp p [] + countp (fun a => decide ¬p a = true) []

case cons
α : Type u_1
l : List α
p q : α → Bool
x : α
h : List α
ih : length h = countp p h + countp (fun a => decide ¬p a = true) h
⊢ length (x :: h) = countp p (x :: h) + countp (fun a => decide ¬p a = true) (x :: h)
α : Type u_1
l✝ : List α
p q : α → Bool
l : List α
⊢ length l = countp p l + countp (fun a => decide ¬p a = true) l
induction' l with x h ih
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)

case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
case cons
α : Type u_1
l : List α
p q : α → Bool
x : α
h : List α
ih : length h = countp p h + countp (fun a => decide ¬p a = true) h
⊢ length (x :: h) = countp p (x :: h) + countp (fun a => decide ¬p a = true) (x :: h)
by_cases h : p x
no goals
case nil
α : Type u_1
l : List α
p q : α → Bool
⊢ length [] = countp p [] + countp (fun a => decide ¬p a = true) []
rfl
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝

α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ ¬(decide ¬p x = true) = true
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
rw [countp_cons_of_pos _ _ h, countp_cons_of_neg _ _ _, length, ih]
no goals
case pos
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 = countp p h✝ + 1 + countp (fun a => decide ¬p a = true) h✝
ac_rfl
no goals
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ ¬(decide ¬p x = true) = true
simp only [h]
case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 =
    countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)

α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ (fun a => decide ¬p a = true) x = true
case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ length (x :: h✝) = countp p (x :: h✝) + countp (fun a => decide ¬p a = true) (x :: h✝)
rw [countp_cons_of_pos (fun a => ¬p a) _ _, countp_cons_of_neg _ _ h, length, ih]
no goals
case neg
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ countp p h✝ + countp (fun a => decide ¬p a = true) h✝ + 1 =
    countp p h✝ + (countp (fun a => decide ¬p a = true) h✝ + 1)
ac_rfl
no goals
α : Type u_1
l : List α
p q : α → Bool
x : α
h✝ : List α
ih : length h✝ = countp p h✝ + countp (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ (fun a => decide ¬p a = true) x = true
simp only [h]