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

State before:
α : Type u
β : Type v
p q : α → Bool
l : List α
h : ∀ (a : α), (p a && q a) = false
⊢ countP (fun a => p a || q a) l = countP p l + countP q l
Tactic:
induction l with
| nil => exact (Nat.zero_add 0).symm
| cons a l IH =>
  simp only [countP_cons]
  specialize h a; revert h
  cases p a <;> cases q a <;> simp [IH]
  . rw [Nat.add_assoc]
  . rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
State after:
no goals

State before:
case nil
α : Type u
β : Type v
p q : α → Bool
h : ∀ (a : α), (p a && q a) = false
⊢ countP (fun a => p a || q a) [] = countP p [] + countP q []
Tactic:
exact (Nat.zero_add 0).symm
State after:
no goals

State before:
case cons
α : Type u
β : Type v
p q : α → Bool
h : ∀ (a : α), (p a && q a) = false
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
h : ∀ (a : α), (p a && q a) = false
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
h : ∀ (a : α), (p a && q a) = false
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:
specialize h a
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
h : (p a && q a) = false
⊢ (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
h : (p a && q a) = false
⊢ (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:
revert h
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
⊢ (p a && q a) = false →
    (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
⊢ (p a && q a) = false →
    (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 [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 p l + countP q 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 p l + countP q l + 1 = countP p l + 1 + countP q l

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 p l + countP q 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 p l + countP q l + 1 = countP p l + 1 + countP q l
Tactic:
. rw [Nat.add_assoc]
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 p l + countP q l + 1 = countP p l + 1 + 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 p l + countP q l + 1 = countP p l + 1 + countP q l
Tactic:
. rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
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 p l + countP q l + 1 = countP p l + (countP q l + 1)
Tactic:
rw [Nat.add_assoc]
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 p l + countP q l + 1 = countP p l + 1 + countP q l
Tactic:
rw [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
State after:
no goals