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

State before:
case nil
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
ha : a ∈ []
⊢ countP p [] = countP p (List.erase [] a) + 1
Tactic:
cases ha
State after:
no goals

State before:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
⊢ countP p (a' :: l) = countP p (List.erase (a' :: l) a) + 1
Tactic:
rewrite [List.erase_cons]
State after:
case cons
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a) + 1

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : a' = a
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a) + 1
Tactic:
cases h
State after:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a :: l
⊢ countP p (a :: l) = countP p (if a = a then l else a :: List.erase l a) + 1

State before:
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a :: l
⊢ countP p (a :: l) = countP p (if a = a then l else a :: List.erase l a) + 1
Tactic:
simp only [if_pos, countP_cons, if_pos hp]
State after:
no goals

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a) + 1
Tactic:
simp only [countP_cons, if_neg h]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ (countP p l + if p a' = true then 1 else 0) = (countP p (List.erase l a) + if p a' = true then 1 else 0) + 1

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ (countP p l + if p a' = true then 1 else 0) = (countP p (List.erase l a) + if p a' = true then 1 else 0) + 1
Tactic:
rewrite [Nat.add_assoc, Nat.add_comm _ 1, ← Nat.add_assoc]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ (countP p l + if p a' = true then 1 else 0) = countP p (List.erase l a) + 1 + if p a' = true then 1 else 0

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p l = countP p (List.erase l a) + 1
Tactic:
exact IH <| (mem_cons.mp ha).resolve_left (Ne.symm h)
State after:
no goals