Theorem: LoVe.List.count_cons (LoVe/LoVelib.lean)

State before:
α : Type
inst✝ : BEq α
x a : α
as : List α
⊢ List.count x (a :: as) = (bif a == x then 1 else 0) + List.count x as
Tactic:
cases Classical.em (a == x) with
| inl hx =>
  rw [List.count, List.countp, List.countp.go, List.countp.go_accum]
  simp [hx]
  ac_rfl
| inr hx =>
  rw [List.count, List.countp, List.countp.go, List.countp]
  simp [hx]
State after:
no goals

State before:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ List.count x (a :: as) = (bif a == x then 1 else 0) + List.count x as
Tactic:
rw [List.count, List.countp, List.countp.go, List.countp.go_accum]
State after:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ (bif a == x then List.countp (fun x_1 => x_1 == x) as + (0 + 1) else List.countp.go (fun x_1 => x_1 == x) as 0) =
    (bif a == x then 1 else 0) + List.countp (fun x_1 => x_1 == x) as

State before:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ (bif a == x then List.countp (fun x_1 => x_1 == x) as + (0 + 1) else List.countp.go (fun x_1 => x_1 == x) as 0) =
    (bif a == x then 1 else 0) + List.countp (fun x_1 => x_1 == x) as
Tactic:
simp [hx]
State after:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ List.countp (fun x_1 => x_1 == x) as + 1 = 1 + List.countp (fun x_1 => x_1 == x) as

State before:
case inl
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : (a == x) = true
⊢ List.countp (fun x_1 => x_1 == x) as + 1 = 1 + List.countp (fun x_1 => x_1 == x) as
Tactic:
ac_rfl
State after:
no goals

State before:
case inr
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : ¬(a == x) = true
⊢ List.count x (a :: as) = (bif a == x then 1 else 0) + List.count x as
Tactic:
rw [List.count, List.countp, List.countp.go, List.countp]
State after:
case inr
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : ¬(a == x) = true
⊢ (bif a == x then List.countp.go (fun x_1 => x_1 == x) as (0 + 1) else List.countp.go (fun x_1 => x_1 == x) as 0) =
    (bif a == x then 1 else 0) + List.countp.go (fun x_1 => x_1 == x) as 0

State before:
case inr
α : Type
inst✝ : BEq α
x a : α
as : List α
hx : ¬(a == x) = true
⊢ (bif a == x then List.countp.go (fun x_1 => x_1 == x) as (0 + 1) else List.countp.go (fun x_1 => x_1 == x) as 0) =
    (bif a == x then 1 else 0) + List.countp.go (fun x_1 => x_1 == x) as 0
Tactic:
simp [hx]
State after:
no goals