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

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

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ List.countP (fun a => decide (p a ∨ q a)) (elems α) =
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Tactic:
simp only [decide_or]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ List.countP (fun a => decide (p a) || decide (q a)) (elems α) =
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ List.countP (fun a => decide (p a) || decide (q a)) (elems α) =
    List.countP (fun a => decide (p a)) (elems α) + List.countP (fun a => decide (q a)) (elems α)
Tactic:
apply List.countP_disjoint
State after:
case h
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ ∀ (a : α), (decide (p a) && decide (q a)) = false

State before:
case h
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ ∀ (a : α), (decide (p a) && decide (q a)) = false
Tactic:
simp only [← decide_and, decide_eq_false_iff_not]
State after:
case h
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ ∀ (a : α), ¬(p a ∧ q a)

State before:
case h
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (a : α), ¬(p a ∧ q a)
⊢ ∀ (a : α), ¬(p a ∧ q a)
Tactic:
exact h
State after:
no goals