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

State before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Tactic:
have := (elems α).countP_image_le_length nodup_elems (f := f)
State after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, a ∈ elems α ∧ f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α

State before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, a ∈ elems α ∧ f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Tactic:
simp only [mem_elems, true_and] at this
State after:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α

State before:
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
this : List.countP (fun b => decide (∃ a, f a = b)) (elems β) ≤ List.length (elems α)
⊢ (count fun b => ∃ a, f a = b) ≤ card α
Tactic:
exact this
State after:
no goals