Theorem: BishopFin.card_eq_count_add_count_not (Fifteen/Logic/BishopFin.lean)

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card α = count p + count fun a => ¬p a
Tactic:
dsimp [card]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (elems α) = count p + count fun a => ¬p a

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (elems α) = count p + count fun a => ¬p a
Tactic:
rewrite [(elems α).length_eq_countP_add_countP p]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun b => decide (p b)) (elems α) + List.countP (fun a => decide ¬decide (p a) = true) (elems α) =
    count p + count fun a => ¬p a

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide ¬decide (p a) = true) (elems α) = count fun a => ¬p a
Tactic:
simp only [decide_eq_true_eq]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide ¬p a) (elems α) = count fun a => ¬p a

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.countP (fun a => decide ¬p a) (elems α) = count fun a => ¬p a
Tactic:
rfl
State after:
no goals