Theorem: List.countP_or_le_add (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
p q : α → Bool
l : List α
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l
Tactic:
induction l with
| nil => exact .refl
| cons a l IH =>
  simp only [countP_cons]
  cases p a <;> cases q a <;> simp only [ite_true, ite_false, Nat.add_zero]
  . exact IH
  . exact Nat.succ_le_succ IH
  . rewrite [Nat.succ_add]; exact Nat.succ_le_succ IH
  . rewrite [Nat.succ_add]; exact Nat.succ_le_succ <| .step IH
State after:
no goals

State before:
case nil
α : Type u
β : Type v
p q : α → Bool
⊢ countP (fun a => p a || q a) [] ≤ countP p [] + countP q []
Tactic:
exact .refl
State after:
no goals

State before:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) (a :: l) ≤ countP p (a :: l) + countP q (a :: l)
Tactic:
simp only [countP_cons]
State after:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) ≤
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)

State before:
case cons
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ (countP (fun a => p a || q a) l + if (p a || q a) = true then 1 else 0) ≤
    (countP p l + if p a = true then 1 else 0) + (countP q l + if q a = true then 1 else 0)
Tactic:
cases p a <;> cases q a <;> simp only [ite_true, ite_false, Nat.add_zero]
State after:
case cons.false.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l

case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)

State before:
case cons.false.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l

case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. exact IH
State after:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)

State before:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)

case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. exact Nat.succ_le_succ IH
State after:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)

State before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l

case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. rewrite [Nat.succ_add]; exact Nat.succ_le_succ IH
State after:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)

State before:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
. rewrite [Nat.succ_add]; exact Nat.succ_le_succ <| .step IH
State after:
no goals

State before:
case cons.false.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l ≤ countP p l + countP q l
Tactic:
exact IH
State after:
no goals

State before:
case cons.false.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + (countP q l + 1)
Tactic:
exact Nat.succ_le_succ IH
State after:
no goals

State before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + countP q l
Tactic:
rewrite [Nat.succ_add]
State after:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + countP q l)

State before:
case cons.true.false
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + countP q l)
Tactic:
exact Nat.succ_le_succ IH
State after:
no goals

State before:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ countP p l + 1 + (countP q l + 1)
Tactic:
rewrite [Nat.succ_add]
State after:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + (countP q l + 1))

State before:
case cons.true.true
α : Type u
β : Type v
p q : α → Bool
a : α
l : List α
IH : countP (fun a => p a || q a) l ≤ countP p l + countP q l
⊢ countP (fun a => p a || q a) l + 1 ≤ Nat.succ (countP p l + (countP q l + 1))
Tactic:
exact Nat.succ_le_succ <| .step IH
State after:
no goals