R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2762655
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2762822
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
d : { x // x ∈ M }
⊢ Localization.add (mk a b) (mk c d) = mk (↑b * c + ↑d * a) (b * d)
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2762655
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2762822
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
d : { x // x ∈ M }
⊢ mk a b + mk c d = mk (↑b * c + ↑d * a) (b * d)
show Localization.add (mk a b) (mk c d) = mk _ _
no goals
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2762655
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2762822
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
d : { x // x ∈ M }
⊢ Localization.add (mk a b) (mk c d) = mk (↑b * c + ↑d * a) (b * d)
simp [Localization.add_def]