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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
have rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
Tactic: rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ 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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
have rw₁ : c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
Tactic: rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ 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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
rw₁ : c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
have rw₂ : c • s • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
Tactic: rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ 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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
rw₁ : c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₂ : c • s • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
have rw₃ : s • c • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
Tactic: rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ 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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
rw₁ : c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₂ : c • s • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₃ : s • c • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
have rw₄ : s • c • (a, b).2 • (a', b').1 = c • (a, b).2 • s • (a', b').1
Tactic: rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ 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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
rw₁ : c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₂ : c • s • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₃ : s • c • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₄ : s • c • (a, b).2 • (a', b').1 = c • (a, b).2 • s • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
have rw₅ : s • c • (a, b).2 • (a', b').1 = c • s • (a, b).2 • (a', b').1
Tactic: rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ 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
s : ↥S
p : LocalizedModule S M
x x_1 : Prod.{v, u} M ↥S
a : M
b : ↥S
a' : M
b' : ↥S
h : (a, b) ≈ (a', b')
c : ↥S
eq1 : c • (a', b').2 • (a, b).1 = c • (a, b).2 • (a', b').1
rw : c • (a', b').2 • s • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
rw₁ : c • (a', b').2 • s • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₂ : c • s • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₃ : s • c • (a', b').2 • (a, b).1 = c • (a, b).2 • s • (a', b').1
rw₄ : s • c • (a, b).2 • (a', b').1 = c • (a, b).2 • s • (a', b').1
rw₅ : s • c • (a, b).2 • (a', b').1 = c • s • (a, b).2 • (a', b').1
⊢ c • ((a', b').2 * s) • (a, b).1 = c • ((a, b).2 * s) • (a', b').1
have rw₆ : s • c • (a, b).2 • (a', b').1 = s • c • (a, b).2 • (a', b').1
Tactic: rw [mul_smul, mul_smul, smul_comm _ s, smul_comm _ s, eq1, smul_comm _ s,
        smul_comm _ 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
s : ↥S
x y : LocalizedModule S M
⊢ (x + y).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (x.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (y.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have refine : ∀ (m m' : M) (s_1 s' : ↥S),
  (HAdd.hAdd (α := LocalizedModule S M) (mk m s_1) (mk m' s')).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      sorry =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m s_1) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry)
      (liftOn (mk m' s') (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry)
Tactic: refine x.induction_on₂ ?_ y
-- 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw : liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry =
  HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry)
    (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry)
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₂ : Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
  (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
simp_rw₂ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₃ : Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
  (mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s)))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
simp_rw₂ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
simp_rw₃ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s)))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₄ : Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
  (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂)))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
simp_rw₂ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
simp_rw₃ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s)))
simp_rw₄ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂)))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₅ : Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
  (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * (t₁ * (s * t₂))))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
simp_rw₂ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
simp_rw₃ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s)))
simp_rw₄ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂)))
simp_rw₅ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * (t₁ * (s * t₂))))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₆ : Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
  (mk (s • t₂ • m₁ + s • t₁ • m₂) (s * (t₁ * (s * t₂))))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
simp_rw₂ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
simp_rw₃ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s)))
simp_rw₄ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂)))
simp_rw₅ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * (t₁ * (s * t₂))))
simp_rw₆ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (s • t₂ • m₁ + s • t₁ • m₂) (s * (t₁ * (s * t₂))))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₇ : Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
  (mk (s • (t₂ • m₁ + t₁ • m₂)) (s * (t₁ * (s * t₂))))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ t₂ : ↥S
simp_rw :
  liftOn (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂)) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
simp_rw₁ : mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s) = HAdd.hAdd (α := LocalizedModule S M) (mk m₁ (t₁ * s)) (mk m₂ (t₂ * s))
simp_rw₂ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk ((t₂ * s) • m₁ + (t₁ * s) • m₂) (t₁ * s * (t₂ * s)))
simp_rw₃ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * t₂ * s))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (t₁ * s * (t₂ * s)))
simp_rw₄ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * t₁ * (s * t₂)))
simp_rw₅ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (t₂ • s • m₁ + t₁ • s • m₂) (s * (t₁ * (s * t₂))))
simp_rw₆ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (s • t₂ • m₁ + s • t₁ • m₂) (s * (t₁ * (s * t₂))))
simp_rw₇ :
  Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (s * (t₁ * t₂)))
    (mk (s • (t₂ • m₁ + t₁ • m₂)) (s * (t₁ * (s * t₂))))
⊢ (HAdd.hAdd (α := LocalizedModule S M) (mk m₁ t₁) (mk m₂ t₂)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s))
      ⋯ =
    HAdd.hAdd (α := LocalizedModule S M) (liftOn (mk m₁ t₁) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
      (liftOn (mk m₂ t₂) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw₈ : Eq (α := LocalizedModule S M) (mk (t₂ • m₁ + t₁ • m₂) (t₁ * (s * t₂)))
  (mk (s • (t₂ • m₁ + t₁ • m₂)) (s * (t₁ * (s * t₂))))
Tactic: simp_rw [mk_add_mk, LocalizedModule.liftOn_mk, mk_add_mk, mul_smul, mul_comm _ s, mul_assoc,
      smul_comm _ s, ← smul_add, mul_left_comm s t₁ t₂, mk_cancel_common_left 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
s : ↥S
r : R
x : LocalizedModule S M
⊢ (r • x).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) r : R)
      (x.liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have refine : ∀ (x : M) (x_1 : ↥S),
  (HSMul.hSMul (β := LocalizedModule S M) r (mk x x_1)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry =
    HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) r : R)
      (liftOn (mk x x_1) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) sorry)
Tactic: refine x.induction_on (fun _ _ ↦ ?_)
-- 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
s : ↥S
r : R
x : LocalizedModule S M
x_1 : M
x_2 : ↥S
⊢ (HSMul.hSMul (β := LocalizedModule S M) r (mk x_1 x_2)).liftOn (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯ =
    HSMul.hSMul (α := R) (β := LocalizedModule S M) ((RingHom.id R : (a : R) → R) r : R)
      (liftOn (mk x_1 x_2) (fun (p : Prod.{v, u} M ↥S) ↦ mk p.1 (p.2 * s)) ⋯)
have simp_rw : Eq (α := LocalizedModule S M) (mk (r • x_1) (x_2 * s))
  (mk (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x_1) (x_2 * s))
Tactic: simp_rw [smul'_mk, liftOn_mk, smul'_mk]