no goals
α : Type u_2
β : Type u_1
γ : Type ?u.3499
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : IsAssociative β gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x₁ x₂ x₃ : α
⊢ f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))
simp only [h.eq, @IsAssociative.assoc _ gb]