-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_erase (a b : α) :
    ∀ l : List α, count a (l.erase b) = count a l - if b == a then 1 else 0
  | [] => by simp
  | c :: l => by
    rw [erase_cons]
    if hc : c = b then
      have hc_beq := beq_iff_eq.mpr hc
      rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
    else
      have hc_beq := beq_false_of_ne hc
      simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l, reduceCtorEq]
      if ha : b = a then
        rw [ha, eq_comm] at hc
        rw [if_pos (beq_iff_eq.2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]
      else
        rw [if_neg (by simpa using ha), Nat.sub_zero, Nat.sub_zero]

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ count a ([].erase b) = count a [] - if (b == a) = true then 1 else 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
hc_beq : (c == b) = false
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Tactic:
simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l, reduceCtorEq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
hc_beq : (c == b) = false
⊢ ((count a l - if (b == a) = true then 1 else 0) + if (c == a) = true then 1 else 0) =
    (count a l + if (c == a) = true then 1 else 0) - if (b == a) = true then 1 else 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : c = b
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Tactic:
have hc_beq := beq_iff_eq.mpr hc

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : c = b
hc_beq : (c == b) = true
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬a = c
hc_beq : (c == b) = false
ha : b = a
⊢ ¬(c == a) = true

Tactic:
simpa using Ne.symm hc

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Tactic:
if hc : c = b then
  have hc_beq := beq_iff_eq.mpr hc
  rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]
else
  have hc_beq := beq_false_of_ne hc
  simp only [hc_beq, if_false, count_cons, count_cons, count_erase a b l, reduceCtorEq]
  if ha : b = a then
    rw [ha, eq_comm] at hc
    rw [if_pos (beq_iff_eq.2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]
  else
    rw [if_neg (by simpa using ha), Nat.sub_zero, Nat.sub_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
hc_beq : (c == b) = false
ha : b = a
⊢ ((count a l - if (b == a) = true then 1 else 0) + if (c == a) = true then 1 else 0) =
    (count a l + if (c == a) = true then 1 else 0) - if (b == a) = true then 1 else 0

Tactic:
rw [ha, eq_comm] at hc

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬a = c
hc_beq : (c == b) = false
ha : b = a
⊢ ((count a l - if (b == a) = true then 1 else 0) + if (c == a) = true then 1 else 0) =
    (count a l + if (c == a) = true then 1 else 0) - if (b == a) = true then 1 else 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
hc_beq : (c == b) = false
ha : ¬b = a
⊢ ((count a l - if (b == a) = true then 1 else 0) + if (c == a) = true then 1 else 0) =
    (count a l + if (c == a) = true then 1 else 0) - if (b == a) = true then 1 else 0

Tactic:
rw [if_neg (by simpa using ha), Nat.sub_zero, Nat.sub_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Tactic:
have hc_beq := beq_false_of_ne hc

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
hc_beq : (c == b) = false
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
hc_beq : (c == b) = false
⊢ ((count a l - if (b == a) = true then 1 else 0) + if (c == a) = true then 1 else 0) =
    (count a l + if (c == a) = true then 1 else 0) - if (b == a) = true then 1 else 0

Tactic:
if ha : b = a then
  rw [ha, eq_comm] at hc
  rw [if_pos (beq_iff_eq.2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]
else
  rw [if_neg (by simpa using ha), Nat.sub_zero, Nat.sub_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬a = c
hc_beq : (c == b) = false
ha : b = a
⊢ ((count a l - if (b == a) = true then 1 else 0) + if (c == a) = true then 1 else 0) =
    (count a l + if (c == a) = true then 1 else 0) - if (b == a) = true then 1 else 0

Tactic:
rw [if_pos (beq_iff_eq.2 ha), if_neg (by simpa using Ne.symm hc), Nat.add_zero, Nat.add_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : ¬c = b
hc_beq : (c == b) = false
ha : ¬b = a
⊢ ¬(b == a) = true

Tactic:
simpa using ha

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
hc : c = b
hc_beq : (c == b) = true
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Tactic:
rw [if_pos hc_beq, hc, count_cons, Nat.add_sub_cancel]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
⊢ count a ((c :: l).erase b) = count a (c :: l) - if (b == a) = true then 1 else 0

Tactic:
rw [erase_cons]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b c : α
l : List α
⊢ count a (if (c == b) = true then l else c :: l.erase b) = count a (c :: l) - if (b == a) = true then 1 else 0