awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ 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) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) (mk m s)
have h : HSMul.hSMul (β := LocalizedModule S M)
    (IsLocalization.mk' T ((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
    (mk m s) =
  IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
    HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2)
      (mk m s)
Tactic: simp_rw [← IsLocalization.mk'_mul, mk'_smul_mk, ← mul_smul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
h :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T ((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1)
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (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 x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2)
      (mk m s) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) (mk m s)
have h₁ : Eq (α := LocalizedModule S M)
  (mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
    ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
  (mk ((IsLocalization.sec S x).1 • (IsLocalization.sec S y).1 • m)
    ((IsLocalization.sec S x).2 * ((IsLocalization.sec S y).2 * s)))
Tactic: simp_rw [← IsLocalization.mk'_mul, mk'_smul_mk, ← mul_smul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
h :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T ((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1)
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) (mk m s)
h₁ :
  Eq (α := LocalizedModule S M)
    (mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
    (mk ((IsLocalization.sec S x).1 • (IsLocalization.sec S y).1 • m)
      ((IsLocalization.sec S x).2 * ((IsLocalization.sec S y).2 * s)))
⊢ 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) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) (mk m s)
have h₂ : Eq (α := LocalizedModule S M)
  (mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
    ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
  (mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
    ((IsLocalization.sec S x).2 * ((IsLocalization.sec S y).2 * s)))
Tactic: simp_rw [← IsLocalization.mk'_mul, mk'_smul_mk, ← mul_smul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
p q : LocalizedModule S M
⊢ x • (p + q) = x • p + x • q
have h : ∀ (m : M) (s : ↥S), x • (mk m s + q) = HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + x • q
Tactic: induction p with | _ m s
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
q : LocalizedModule S M
m : M
s : ↥S
⊢ x • (mk m s + q) = HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + x • q
have h : ∀ (n : M) (t : ↥S),
  x • HAdd.hAdd (α := LocalizedModule S M) (mk m s) (mk n t) =
    HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + HSMul.hSMul (β := LocalizedModule S M) x (mk n t)
Tactic: induction q with | _ n t
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
⊢ x • HAdd.hAdd (α := LocalizedModule S M) (mk m s) (mk n t) =
    HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + HSMul.hSMul (β := LocalizedModule S M) x (mk n t)
have h : HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
  mk
    (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
    ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
Tactic: rw [smul_def, smul_def, mk_add_mk, mk_add_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
    HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk (t • m + s • n) (s * t))
have rw : HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
  HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t))
Tactic: rw [IsLocalization.mk'_sec (M := S) T]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
have h : HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
    (mk (t • m + s • n) (s * t)) =
  mk
    (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
    ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
Tactic: rw [show x • _ = IsLocalization.mk' T _ _ • _ by rw [IsLocalization.mk'_sec (M := S) T]]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk (t • m + s • n) (s * t)) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
have h : Eq (α := LocalizedModule S M)
  (mk (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n))
    ((IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t)))
  (mk
    (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
    ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)))
Tactic: rw [← IsLocalization.mk'_cancel _ _ (IsLocalization.sec S x).2, mk'_smul_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
⊢ Eq (α := LocalizedModule S M)
    (mk (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n))
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t)))
    (mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)))
have h : ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n) =
  ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
    ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
h :
  ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n
⊢ Eq (α := LocalizedModule S M)
    (mk (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n))
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t)))
    (mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)))
have h₁ : (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
  (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n
have h : ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R) * (↑t : R)) • m +
    ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R) * (↑s : R)) • n =
  ((↑(IsLocalization.sec S x).2 : R) * (↑t : R) * (IsLocalization.sec S x).1) • m +
    ((↑(IsLocalization.sec S x).2 : R) * (↑s : R) * (IsLocalization.sec S x).1) • n
Tactic: simp only [Submonoid.smul_def, smul_add, ← mul_smul, Submonoid.coe_mul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
have h : (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t) =
  (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
Tactic: rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
| HSMul.hSMul (β := LocalizedModule S M) x 0 = 0
have lhs : HSMul.hSMul (β := LocalizedModule S M) x 0
Tactic: lhs
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
| HSMul.hSMul (β := LocalizedModule S M) x 0
have rw : 0
Tactic: rw [← zero_mk 1, smul_def, smul_zero, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
| HSMul.hSMul (β := LocalizedModule S M) x 0 = 0
have rw : 0
Tactic: lhs; rw [← zero_mk 1, smul_def, smul_zero, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
⊢ HSMul.hSMul (β := LocalizedModule S M) x 0 = 0
have conv : HSMul.hSMul (β := LocalizedModule S M) x 0 = 0
Tactic: conv => lhs; rw [← zero_mk 1, smul_def, smul_zero, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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 : T
conv : HSMul.hSMul (β := LocalizedModule S M) x 0 = 0
⊢ HSMul.hSMul (β := LocalizedModule S M) x 0 = 0
have conv₁ : Eq (α := LocalizedModule S M) 0 0
Tactic: conv => lhs; rw [← zero_mk 1, smul_def, smul_zero, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
p : LocalizedModule S M
⊢ (x + y) • p = x • p + y • p
have h : ∀ (m : M) (s : ↥S),
  HSMul.hSMul (β := LocalizedModule S M) (x + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + HSMul.hSMul (β := LocalizedModule S M) y (mk m s)
Tactic: induction p with | _ m s
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s]