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

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ count p = card { a // p a }
Tactic:
dsimp [count]
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 α) = card { 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 α) = card { a // p a }
Tactic:
rewrite [List.countP_eq_length_filter]
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = card { a // p a }

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = card { a // p a }
Tactic:
conv => rhs; change subtype (p:=p) |>.elems' |>.length
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = List.length elems'

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) = List.length elems'
Tactic:
dsimp [elems']
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) =
    List.length
      (List.pmap Subtype.mk (List.filter (fun a => decide (p a)) (elems α))
        (_ : ∀ (a : α), a ∈ List.filter (fun a => decide (p a)) (elems α) → p a))

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ List.length (List.filter (fun a => decide (p a)) (elems α)) =
    List.length
      (List.pmap Subtype.mk (List.filter (fun a => decide (p a)) (elems α))
        (_ : ∀ (a : α), a ∈ List.filter (fun a => decide (p a)) (elems α) → p a))
Tactic:
simp only [List.length_pmap]
State after:
no goals