no goals
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Distrib R
a b x y : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a + b) x y
simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]