exact s1 a
case h.h₁.a.mpr
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
a1 : x = finv a
s1 : ∀ (x : β), f (finv x) = x
⊢ f (finv a) = a
no goals