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

State before:
α : Type
inst✝ : BEq α
x : α
as bs : List α
⊢ List.count x (as ++ bs) = List.count x as + List.count x bs
Tactic:
induction as with
| nil           => simp
| cons a as' ih =>
  simp [ih]
  ac_rfl
State after:
no goals

State before:
case nil
α : Type
inst✝ : BEq α
x : α
bs : List α
⊢ List.count x ([] ++ bs) = List.count x [] + List.count x bs
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type
inst✝ : BEq α
x : α
bs : List α
a : α
as' : List α
ih : List.count x (as' ++ bs) = List.count x as' + List.count x bs
⊢ List.count x (a :: as' ++ bs) = List.count x (a :: as') + List.count x bs
Tactic:
simp [ih]
State after:
case cons
α : Type
inst✝ : BEq α
x : α
bs : List α
a : α
as' : List α
ih : List.count x (as' ++ bs) = List.count x as' + List.count x bs
⊢ (bif a == x then 1 else 0) + (List.count x as' + List.count x bs) =
    (bif a == x then 1 else 0) + List.count x as' + List.count x bs

State before:
case cons
α : Type
inst✝ : BEq α
x : α
bs : List α
a : α
as' : List α
ih : List.count x (as' ++ bs) = List.count x as' + List.count x bs
⊢ (bif a == x then 1 else 0) + (List.count x as' + List.count x bs) =
    (bif a == x then 1 else 0) + List.count x as' + List.count x bs
Tactic:
ac_rfl
State after:
no goals