-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x y : T
m : M
s : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 +
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2)
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₂ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₃ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s)
rw₄ : R
rw₅ : ↥S
rw₆ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s)
rw₇ : R
rw₈ : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) (x + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)

Tactic:
rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s]

Premises used: IsLocalization.mk'_sec, IsLocalization.mk'_cancel, IsLocalization.mk'_add