no goals
α : Type ?u.23
M₀ : Type ?u.26
G₀ : Type u_1
M₀' : Type ?u.32
G₀' : Type ?u.35
F : Type ?u.38
F' : Type ?u.41
inst✝ : MulZeroClass G₀
a : G₀
⊢ SemiconjBy a 0 0
simp only [SemiconjBy, mul_zero, zero_mul]