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

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

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ List.countP (fun a => decide (p a)) (elems α) ≤ 1
Tactic:
refine List.countP_le_one_of_unique_nodup ?_ nodup_elems
State after:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), decide (p a) = true → decide (p b) = true → a = b

State before:
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), decide (p a) = true → decide (p b) = true → a = b
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
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), p a → p b → a = b

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