no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1160
f fab : α → β
fbc : β → γ
ga ga' : α → α
gb gb' : β → β
gc gc' : γ → γ
h : Semiconj f ga gb
ha : RightInverse ga' ga
hb : LeftInverse gb' gb
x : α
⊢ f (ga' x) = gb' (f x)
rw [← hb (f (ga' x)), ← h.eq, ha x]