apply Subtype.eq
case f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ y₁ = y₂
case f_inj.a
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
f : β → α
f_inj : ∀ (b₁ b₂ : β), f b₁ = f b₂ → b₁ = b₂
y₁ y₂ : { a // (p ∘ f) a }
h : { val := f y₁.val, property := (_ : (p ∘ f) y₁.val) } = { val := f y₂.val, property := (_ : (p ∘ f) y₂.val) }
⊢ y₁.val = y₂.val