congr!
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ (if f x = a then b else g (f x)) = if x = finv a then b else (g ∘ f) x
case h.h₁.a
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ f x = a ↔ x = finv a