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 : T
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ Eq (α := LocalizedModule S M) ((fun (p : Prod.{v, u} M ↥S) ↦ (mk (a.1 • p.1) (a.2 * p.2) : LocalizedModule S M)) p)
    ((fun (p : Prod.{v, u} M ↥S) ↦ (mk (a.1 • p.1) (a.2 * p.2) : LocalizedModule S M)) p')
have refine : s • (a.2 * p'.2) • a.1 • p.1 = s • (a.2 * p.2) • a.1 • p'.1
Tactic: refine mk_eq.mpr ⟨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 : T
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1
have simp_rw : ((↑s : R) * ((↑a.2 : R) * (↑p'.2 : R) * a.1)) • p.1 = ((↑a.2 : R) * (a.1 * ((↑s : R) * (↑p'.2 : R)))) • p.1
Tactic: simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]
-- 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_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ a.2 • a.1 • s • p'.2 • p.1 = a.2 • a.1 • s • p.2 • p'.1
have rw : a.2 • a.1 • s • p.2 • p'.1 = a.2 • a.1 • s • p.2 • p'.1
Tactic: rw [h]
-- 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_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ a.2 • a.1 • s • p.2 • p'.1 = s • (a.2 * p.2) • a.1 • p'.1
have simp_rw : ((↑a.2 : R) * (a.1 * ((↑s : R) * (↑p.2 : R)))) • p'.1 = ((↑s : R) * ((↑a.2 : R) * (↑p.2 : R) * a.1)) • p'.1
Tactic: simp_rw [Submonoid.smul_def, ← 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
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = s • (a.2 * p.2) • a.1 • p'.1
have _ : s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1
Tactic: calc
          _ = a.2 • a.1 • s • p'.2 • p.1 := by
            simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]; ring_nf
          _ = a.2 • a.1 • s • p.2 • p'.1 := by rw [h]
          _ = s • (a.2 * p.2) • a.1 • p'.1 := by
            simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]; ring_nf
-- 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_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
_ : s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = s • (a.2 * p.2) • a.1 • p'.1
have _₁ : a.2 • a.1 • s • p'.2 • p.1 = a.2 • a.1 • s • p.2 • p'.1
Tactic: calc
          _ = a.2 • a.1 • s • p'.2 • p.1 := by
            simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]; ring_nf
          _ = a.2 • a.1 • s • p.2 • p'.1 := by rw [h]
          _ = s • (a.2 * p.2) • a.1 • p'.1 := by
            simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]; ring_nf
-- 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_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
_ : s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1
_₁ : a.2 • a.1 • s • p'.2 • p.1 = a.2 • a.1 • s • p.2 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = s • (a.2 * p.2) • a.1 • p'.1
have _₂ : a.2 • a.1 • s • p.2 • p'.1 = s • (a.2 * p.2) • a.1 • p'.1
Tactic: calc
          _ = a.2 • a.1 • s • p'.2 • p.1 := by
            simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]; ring_nf
          _ = a.2 • a.1 • s • p.2 • p'.1 := by rw [h]
          _ = s • (a.2 * p.2) • a.1 • p'.1 := by
            simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]; ring_nf
-- 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
r : R
m : M
s s' : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T r s) (mk m s') = mk (r • m) (s * s')
have rw : ∃ (u : ↥S),
  u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
Tactic: rw [smul_def, mk_eq]
-- 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
r : R
m : M
s s' : ↥S
⊢ ∃ (u : ↥S),
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have obtain : ∀ (c : ↥S)
  (hc :
    (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
      (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)),
  ∃ (u : ↥S),
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
Tactic: obtain ⟨c, hc⟩ := IsLocalization.eq.mp <| IsLocalization.mk'_sec T (IsLocalization.mk' T r 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
⊢ ∃ (u : ↥S),
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h : c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
  c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
Tactic: use c
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h : (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
  (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
Tactic: simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h₁ : (↑(c * (s * s')) : R) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
  (↑(c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) : R) • r • m
Tactic: simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
h₁ :
  (↑(c * (s * s')) : R) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (↑(c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) : R) • r • m
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h₂ : ((↑c : R) * ((↑s : R) * (↑s' : R))) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
  ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R))) • r • m
Tactic: simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
h₁ :
  (↑(c * (s * s')) : R) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (↑(c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) : R) • r • m
h₂ :
  ((↑c : R) * ((↑s : R) * (↑s' : R))) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R))) • r • m
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h₃ : ((↑c : R) * ((↑s : R) * (↑s' : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
  ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R)) * r) • m
Tactic: simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
h₁ :
  (↑(c * (s * s')) : R) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (↑(c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) : R) • r • m
h₂ :
  ((↑c : R) * ((↑s : R) * (↑s' : R))) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R))) • r • m
h₃ :
  ((↑c : R) * ((↑s : R) * (↑s' : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R)) * r) • m
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h₄ : ((↑c : R) * (↑s : R) * (↑s' : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
  ((↑c : R) * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R) * r) • m
Tactic: simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
h₁ :
  (↑(c * (s * s')) : R) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (↑(c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) : R) • r • m
h₂ :
  ((↑c : R) * ((↑s : R) * (↑s' : R))) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R))) • r • m
h₃ :
  ((↑c : R) * ((↑s : R) * (↑s' : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R)) * r) • m
h₄ :
  ((↑c : R) * (↑s : R) * (↑s' : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑c : R) * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R) * r) • m
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h₅ : ((↑s' : R) * ((↑c : R) * (↑s : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
  ((↑s' : R) * ((↑c : R) * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R)) * r) • m
Tactic: simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
h₁ :
  (↑(c * (s * s')) : R) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (↑(c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) : R) • r • m
h₂ :
  ((↑c : R) * ((↑s : R) * (↑s' : R))) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R))) • r • m
h₃ :
  ((↑c : R) * ((↑s : R) * (↑s' : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R)) * r) • m
h₄ :
  ((↑c : R) * (↑s : R) * (↑s' : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑c : R) * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R) * r) • m
h₅ :
  ((↑s' : R) * ((↑c : R) * (↑s : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑s' : R) * ((↑c : R) * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R)) * r) • m
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
have h₆ : ((↑s' : R) * ((↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1))) • m =
  ((↑s' : R) * ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r))) • m
Tactic: simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]
-- 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
r : R
m : M
s t : ↥S
⊢ Eq (α := OreLocalization S M) (r • m /ₒ (t * s)) (mk (r • m) (s * t))
have rw : Eq (α := OreLocalization S M) (r • m /ₒ (s * t)) (mk (r • m) (s * t))
Tactic: rw [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
p : LocalizedModule S M
⊢ HSMul.hSMul (α := T) 1 p = p
have h : ∀ (m : M) (s : ↥S), HSMul.hSMul (α := T) (β := LocalizedModule S M) 1 (mk m s) = 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
m : M
s : ↥S
⊢ 1 = IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1
have rw : Eq.{u_1 + 1} (α := T) (1 : T) ((algebraMap R T : (a : R) → T) 1 : T)
Tactic: rw [IsLocalization.mk'_one, map_one]
-- 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
m : M
s : ↥S
rw : Eq.{u_1 + 1} (α := T) (1 : T) ((algebraMap R T : (a : R) → T) 1 : T)
⊢ 1 = IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1
have rw₁ : Eq.{u_1 + 1} (α := T) 1 1
Tactic: rw [IsLocalization.mk'_one, map_one]
-- 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
m : M
s : ↥S
⊢ HSMul.hSMul (α := T) (β := LocalizedModule S M) 1 (mk m s) = mk m s
have h : HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1) (mk m s) = mk m s
Tactic: rw [show (1 : T) = IsLocalization.mk' T (1 : R) (1 : S) by rw [IsLocalization.mk'_one, map_one]]
-- 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
m : M
s : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1) (mk m s) = mk m s
have h : Eq (α := LocalizedModule S M) (mk (HSMul.hSMul.{u, v, v} (α := R) 1 m) (1 * s)) (mk m s)
Tactic: rw [mk'_smul_mk, one_smul, one_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
m : M
s : ↥S
h : Eq (α := LocalizedModule S M) (mk (HSMul.hSMul.{u, v, v} (α := R) 1 m) (1 * s)) (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1) (mk m s) = mk m s
have h₁ : Eq (α := LocalizedModule S M) (mk m (1 * s)) (mk m s)
Tactic: rw [mk'_smul_mk, one_smul, one_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
m : M
s : ↥S
h : Eq (α := LocalizedModule S M) (mk (HSMul.hSMul.{u, v, v} (α := R) 1 m) (1 * s)) (mk m s)
h₁ : Eq (α := LocalizedModule S M) (mk m (1 * s)) (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1) (mk m s) = mk m s
have h₂ : Eq (α := LocalizedModule S M) (mk m s) (mk m s)
Tactic: rw [mk'_smul_mk, one_smul, one_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 y : T
p : LocalizedModule S M
⊢ (x * y) • p = x • y • p
have h : ∀ (m : M) (s : ↥S),
  HSMul.hSMul (β := LocalizedModule S M) (x * y) (mk m s) = x • 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) = x • HSMul.hSMul (β := LocalizedModule S M) y (mk m s)
have h : 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)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y]