no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3743
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsIdempotent α ga
h : Semiconj₂ f ga gb
h_surj : Surjective f
x : α
⊢ gb (f x) (f x) = f x
simp only [← h.eq, @IsIdempotent.idempotent _ ga]