no goals
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type ?u.2970634
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.2970871
inst✝ : CommRing P
a c : R
b d : { x // x ∈ M }
⊢ mk a b + -mk c d = mk a b + mk (-c) d
rw [neg_mk]
case e_x
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type ?u.2970634
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.2970871
inst✝ : CommRing P
a c : R
b d : { x // x ∈ M }
⊢ ↑b * -c + ↑d * a = ↑d * a - ↑b * c
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type ?u.2970634
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.2970871
inst✝ : CommRing P
a c : R
b d : { x // x ∈ M }
⊢ mk (↑b * -c + ↑d * a) (b * d) = mk (↑d * a - ↑b * c) (b * d)
congr
no goals
case e_x
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type ?u.2970634
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.2970871
inst✝ : CommRing P
a c : R
b d : { x // x ∈ M }
⊢ ↑b * -c + ↑d * a = ↑d * a - ↑b * c
ring