R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.894644
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : { x // x ∈ M }
⊢ ↑(algebraMap R ((fun x => (fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂)) (↑(y₁ * y₂) * x₁))) (↑y₁ * ↑(y₁ * y₂) * x₂) +
      ↑(algebraMap R ((fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂))) (↑(y₁ * y₂) * x₁) *
        ↑(algebraMap R ((fun x => (fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂)) (↑(y₁ * y₂) * x₁))) ↑y₂ =
    ↑(algebraMap R S) (x₂ * ↑y₁ + x₁ * ↑y₂) * ↑(algebraMap R ((fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂))) ↑y₁ *
      ↑(algebraMap R ((fun x => (fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂)) (↑(y₁ * y₂) * x₁))) ↑y₂
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.894644
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : { x // x ∈ M }
⊢ (mk' S x₁ y₁ + mk' S x₂ y₂) * ↑(algebraMap R S) ↑(y₁ * y₂) = ↑(algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁)
rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
  mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul,
  add_comm _ (mk' _ _ _), mk'_add_eq_iff_add_mul_eq_mul]
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.894644
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : { x // x ∈ M }
⊢ ↑(algebraMap R S) ↑y₁ * (↑(algebraMap R S) ↑y₁ * ↑(algebraMap R S) ↑y₂) * ↑(algebraMap R S) x₂ +
      ↑(algebraMap R S) ↑y₁ * ↑(algebraMap R S) ↑y₂ * ↑(algebraMap R S) x₁ * ↑(algebraMap R S) ↑y₂ =
    (↑(algebraMap R S) x₂ * ↑(algebraMap R S) ↑y₁ + ↑(algebraMap R S) x₁ * ↑(algebraMap R S) ↑y₂) *
        ↑(algebraMap R S) ↑y₁ *
      ↑(algebraMap R S) ↑y₂
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.894644
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : { x // x ∈ M }
⊢ ↑(algebraMap R ((fun x => (fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂)) (↑(y₁ * y₂) * x₁))) (↑y₁ * ↑(y₁ * y₂) * x₂) +
      ↑(algebraMap R ((fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂))) (↑(y₁ * y₂) * x₁) *
        ↑(algebraMap R ((fun x => (fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂)) (↑(y₁ * y₂) * x₁))) ↑y₂ =
    ↑(algebraMap R S) (x₂ * ↑y₁ + x₁ * ↑y₂) * ↑(algebraMap R ((fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂))) ↑y₁ *
      ↑(algebraMap R ((fun x => (fun x => S) (x₂ * ↑y₁ + x₁ * ↑y₂)) (↑(y₁ * y₂) * x₁))) ↑y₂
simp only [map_add, Submonoid.coe_mul, map_mul]
no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.894644
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : { x // x ∈ M }
⊢ ↑(algebraMap R S) ↑y₁ * (↑(algebraMap R S) ↑y₁ * ↑(algebraMap R S) ↑y₂) * ↑(algebraMap R S) x₂ +
      ↑(algebraMap R S) ↑y₁ * ↑(algebraMap R S) ↑y₂ * ↑(algebraMap R S) x₁ * ↑(algebraMap R S) ↑y₂ =
    (↑(algebraMap R S) x₂ * ↑(algebraMap R S) ↑y₁ + ↑(algebraMap R S) x₁ * ↑(algebraMap R S) ↑y₂) *
        ↑(algebraMap R S) ↑y₁ *
      ↑(algebraMap R S) ↑y₂
ring