R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2768138
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2768305
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
⊢ ↑(r' M) (↑b * c + ↑b * a, b * b) (a + c, b)
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2768138
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2768305
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
⊢ mk a b + mk c b = mk (a + c) b
rw [add_mk, mk_eq_mk_iff, r_eq_r']
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2768138
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2768305
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
⊢ ↑1 * (↑(↑b * c + ↑b * a, b * b).snd * (a + c, b).fst) = ↑1 * (↑(a + c, b).snd * (↑b * c + ↑b * a, b * b).fst)
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2768138
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2768305
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
⊢ ↑(r' M) (↑b * c + ↑b * a, b * b) (a + c, b)
refine' (r' M).symm ⟨1, _⟩
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2768138
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2768305
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
⊢ 1 * (↑b * ↑b * (a + c)) = 1 * (↑b * (↑b * c + ↑b * a))
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2768138
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2768305
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
⊢ ↑1 * (↑(↑b * c + ↑b * a, b * b).snd * (a + c, b).fst) = ↑1 * (↑(a + c, b).snd * (↑b * c + ↑b * a, b * b).fst)
simp only [Submonoid.coe_one, Submonoid.coe_mul]
no goals
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2768138
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2768305
inst✝ : CommSemiring P
a : R
b : { x // x ∈ M }
c : R
⊢ 1 * (↑b * ↑b * (a + c)) = 1 * (↑b * (↑b * c + ↑b * a))
ring