rw [← hgf a₁, ← hgf a₂, hfa]
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
a₁ a₂ : α
hfa : f a₁ = f a₂
⊢ a₁ = a₂
no goals