. intro h; let ⟨a,hpa,hfa⟩ := h
  exact ⟨⟨a,hpa⟩, hfa⟩
case h.mp
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, p a ∧ f a = b) → ∃ a, (f ∘ Subtype.val) a = b

case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, (f ∘ Subtype.val) a = b) → ∃ a, p a ∧ f a = b
case h.mpr
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq β
f : α → β
b : β
⊢ (∃ a, (f ∘ Subtype.val) a = b) → ∃ a, p a ∧ f a = b