no goals
α : Type ?u.307
M₀ : Type ?u.310
G₀ : Type u_1
M₀' : Type ?u.316
G₀' : Type ?u.319
F : Type ?u.322
F' : Type ?u.325
inst✝ : MulZeroClass G₀
x y : G₀
⊢ SemiconjBy 0 x y
simp only [SemiconjBy, mul_zero, zero_mul]