let ⟨a,b,ha⟩ := x
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
x : { a // ∃ b, f b = a }
a✝ : x ∈ elems { a // ∃ b, f b = a }
⊢ ∃ a, a ∈ elems β ∧ { val := f a, property := (_ : ∃ b, f b = f a) } = x
α : Type u
β : Type v
inst✝⁴ : BishopFin α
inst✝³ : BishopFin β
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
f : β → α
hf : ∀ (a : α), p a → ∃ b, f b = a
f' : β → { a // ∃ b, f b = a } := fun b => { val := f b, property := (_ : ∃ b_1, f b_1 = f b) }
this : f = Subtype.val ∘ f'
x : { a // ∃ b, f b = a }
a : α
b : β
ha : f b = a
a✝ : { val := a, property := (_ : ∃ b, f b = a) } ∈ elems { a // ∃ b, f b = a }
⊢ ∃ a_1,
    a_1 ∈ elems β ∧ { val := f a_1, property := (_ : ∃ b, f b = f a_1) } = { val := a, property := (_ : ∃ b, f b = a) }