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

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

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

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

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

State before:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a)
Tactic:
simp only [countP_cons, if_neg h]
State after:
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
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

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