-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Count.lean
theorem countP_set (p : α → Bool) (l : List α) (i : Nat) (a : α) (h : i < l.length) :
    (l.set i a).countP p = l.countP p - (if p l[i] then 1 else 0) + (if p a then 1 else 0)

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h✝ : i + 1 < (x :: l).length
h : i < l.length
⊢ (((countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0) + if p x = true then 1 else 0) =
    ((countP p l + if p x = true then 1 else 0) - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
have : (if p l[i] = true then 1 else 0) ≤ l.countP p := boole_getElem_le_countP p l i h

Result:
case cons.succ
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h✝ : i + 1 < (x :: l).length
h : i < l.length
this : (if p l[i] = true then 1 else 0) ≤ countP p l
⊢ (((countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0) + if p x = true then 1 else 0) =
    ((countP p l + if p x = true then 1 else 0) - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h : i + 1 < (x :: l).length
⊢ countP p ((x :: l).set (i + 1) a) =
    (countP p (x :: l) - if p (x :: l)[i + 1] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
simp [add_one_lt_add_one_iff] at h

Result:
case cons.succ
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h✝ : i + 1 < (x :: l).length
h : i < l.length
⊢ countP p ((x :: l).set (i + 1) a) =
    (countP p (x :: l) - if p (x :: l)[i + 1] = true then 1 else 0) + if p a = true then 1 else 0

Proof state:
α : Type u_1
p : α → Bool
l : List α
i : Nat
a : α
h : i < l.length
⊢ countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
induction l generalizing i with
| nil => simp at h
| cons x l ih =>
  cases i with
  | zero => simp [countP_cons]
  | succ i =>
    simp [add_one_lt_add_one_iff] at h
    simp [countP_cons, ih _ h]
    have : (if p l[i] = true then 1 else 0) ≤ l.countP p := boole_getElem_le_countP p l i h
    omega

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h : i < (x :: l).length
⊢ countP p ((x :: l).set i a) =
    (countP p (x :: l) - if p (x :: l)[i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
cases i with
| zero => simp [countP_cons]
| succ i =>
  simp [add_one_lt_add_one_iff] at h
  simp [countP_cons, ih _ h]
  have : (if p l[i] = true then 1 else 0) ≤ l.countP p := boole_getElem_le_countP p l i h
  omega

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h✝ : i + 1 < (x :: l).length
h : i < l.length
⊢ countP p ((x :: l).set (i + 1) a) =
    (countP p (x :: l) - if p (x :: l)[i + 1] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
simp [countP_cons, ih _ h]

Result:
case cons.succ
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h✝ : i + 1 < (x :: l).length
h : i < l.length
⊢ (((countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0) + if p x = true then 1 else 0) =
    ((countP p l + if p x = true then 1 else 0) - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

Proof state:
case cons.zero
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
h : 0 < (x :: l).length
⊢ countP p ((x :: l).set 0 a) =
    (countP p (x :: l) - if p (x :: l)[0] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
simp [countP_cons]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
a : α
i : Nat
h : i < [].length
⊢ countP p ([].set i a) = (countP p [] - if p [][i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
p : α → Bool
a x : α
l : List α
ih :
  ∀ (i : Nat) (h : i < l.length),
    countP p (l.set i a) = (countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0
i : Nat
h✝ : i + 1 < (x :: l).length
h : i < l.length
this : (if p l[i] = true then 1 else 0) ≤ countP p l
⊢ (((countP p l - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0) + if p x = true then 1 else 0) =
    ((countP p l + if p x = true then 1 else 0) - if p l[i] = true then 1 else 0) + if p a = true then 1 else 0

Tactic:
omega

Result:
no goals