no goals
α : Type u_2
β : Type u_1
γ : Type ?u.3984
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsIdempotent β gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x
rw [h.eq, @IsIdempotent.idempotent _ gb]