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

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

Tactic:
induction l generalizing i with
| nil => simp at h
| cons x l ih =>
  cases i with
  | zero => simp [countP_cons]
  | succ i =>
    simp only [length_cons, add_one_lt_add_one_iff] at h
    simp only [getElem_cons_succ, countP_cons]
    specialize ih _ h
    exact le_add_right_of_le ih

Result:
no goals

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

Tactic:
exact le_add_right_of_le ih

Result:
no goals

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

Tactic:
simp only [getElem_cons_succ, countP_cons]

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

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

Tactic:
simp only [length_cons, add_one_lt_add_one_iff] at h

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

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

Tactic:
simp at h

Result:
no goals

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

Tactic:
cases i with
| zero => simp [countP_cons]
| succ i =>
  simp only [length_cons, add_one_lt_add_one_iff] at h
  simp only [getElem_cons_succ, countP_cons]
  specialize ih _ h
  exact le_add_right_of_le ih

Result:
no goals

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

Tactic:
specialize ih _ h

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

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

Tactic:
simp [countP_cons]

Result:
no goals