Theorem: List.countp_cons (One.lean)

State before:
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp p (head :: tail) = (if p head = true then 1 else 0) + countp p tail
Tactic:
rw [countp, countp.go]
State after:
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif p head then countp.go p tail (0 + 1) else countp.go p tail 0) = (if p head = true then 1 else 0) + countp p tail

State before:
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif p head then countp.go p tail (0 + 1) else countp.go p tail 0) = (if p head = true then 1 else 0) + countp p tail
Tactic:
cases p head with
| true => simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_true, ite_true]; rw [List.countp.go_acc, ← countp]
| false => simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_false, ite_false]; rw [← countp]
State after:
no goals

State before:
case true
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif true then countp.go p tail (0 + 1) else countp.go p tail 0) = (if true = true then 1 else 0) + countp p tail
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_true, ite_true]
State after:
case true
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 1 = 1 + countp p tail

State before:
case true
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 1 = 1 + countp p tail
Tactic:
rw [List.countp.go_acc, ← countp]
State after:
no goals

State before:
case false
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ (bif false then countp.go p tail (0 + 1) else countp.go p tail 0) = (if false = true then 1 else 0) + countp p tail
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_add, cond_false, ite_false]
State after:
case false
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 0 = countp p tail

State before:
case false
α : Type u_1
p : α → Bool
head : α
tail : List α
⊢ countp.go p tail 0 = countp p tail
Tactic:
rw [← countp]
State after:
no goals