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

State before:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ card { a // p a } ≤ card α
Tactic:
apply card_le_card_of_inj Subtype.val
State after:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ ∀ (a₁ a₂ : { a // p a }), a₁.val = a₂.val → a₁ = a₂

State before:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
⊢ ∀ (a₁ a₂ : { a // p a }), a₁.val = a₂.val → a₁ = a₂
Tactic:
intro _ _
State after:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
a₁✝ a₂✝ : { a // p a }
⊢ a₁✝.val = a₂✝.val → a₁✝ = a₂✝

State before:
α : Type u
p : α → Prop
inst✝¹ : BishopFin α
inst✝ : DecidablePred p
a₁✝ a₂✝ : { a // p a }
⊢ a₁✝.val = a₂✝.val → a₁✝ = a₂✝
Tactic:
exact Subtype.eq
State after:
no goals