case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ countp.go p (a :: l) 0 = countp.go p l 1

α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp p (a :: l) = countp p l + 1
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ countp p (a :: l) = countp p l + 1
have : countp.go p (a :: l) 0 = countp.go p l 1
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp.go p (a :: l) 0 = countp.go p l 0 + 1
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp p (a :: l) = countp p l + 1
unfold countp
no goals
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
this : countp.go p (a :: l) 0 = countp.go p l 1
⊢ countp.go p (a :: l) 0 = countp.go p l 0 + 1
rw [this, add_comm, List.countp_go_eq_add]
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ countp.go p (a :: l) 0 = countp.go p l 1
change (bif _ then _ else _) = countp.go _ _ _
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif true then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif p a then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
rw [pa]
no goals
case this
α : Type u_1
l✝ : List α
p q : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif true then countp.go p l (0 + 1) else countp.go p l 0) = countp.go p l 1
rfl