[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : Distrib R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x + x') (y + y')
[PROOFSTEP]
simp only [SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]
[GOAL]
α : 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
[PROOFSTEP]
simp only [SemiconjBy, left_distrib, right_distrib, ha.eq, hb.eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy a (-x) (-y)
[PROOFSTEP]
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy (-a) x y
[PROOFSTEP]
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x - x') (y - y')
[PROOFSTEP]
simpa only [sub_eq_add_neg] using h.add_right h'.neg_right
[GOAL]
α : Type u
β : Type v
γ : Type w
R : Type x
inst✝ : NonUnitalNonAssocRing R
a b x y x' y' : R
ha : SemiconjBy a x y
hb : SemiconjBy b x y
⊢ SemiconjBy (a - b) x y
[PROOFSTEP]
simpa only [sub_eq_add_neg] using ha.add_left hb.neg_left
