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
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
h : a • t • r • m = a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m
h₁ : a • t • r • m = a • (t * Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) • m
⊢ a • t • r • m = a • s • n
have h₂ : a • t • r • m = a • t • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
Tactic: rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_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
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
h : a • t • r • m = a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m
h₁ : a • t • r • m = a • (t * Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) • m
h₂ : a • t • r • m = a • t • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
⊢ a • t • r • m = a • s • n
have h₃ : a • (↑t : R) • r • m = a • t • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
Tactic: rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_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
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
h : a • t • r • m = a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m
h₁ : a • t • r • m = a • (t * Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) • m
h₂ : a • t • r • m = a • t • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
h₃ : a • (↑t : R) • r • m = a • t • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
⊢ a • t • r • m = a • s • n
have h₄ : a • (↑t : R) • r • m = a • (↑t : R) • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
Tactic: rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_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
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
h : a • t • r • m = a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m
h₁ : a • t • r • m = a • (t * Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr) • m
h₂ : a • t • r • m = a • t • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
h₃ : a • (↑t : R) • r • m = a • t • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
h₄ : a • (↑t : R) • r • m = a • (↑t : R) • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • m
⊢ a • t • r • m = a • s • n
have h₅ : a • (↑t : R) • r • m = a • (↑t : R) • r • m
Tactic: rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_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
r : R
hr : r ∈ S
y : LocalizedModule S M
m : M
s : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) r (mk m s) = y ↔
    mk m s =
      HSMul.hSMul (α := Localization (M := R) S) (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) y
have h : ∀ (n : M) (t : ↥S),
  HSMul.hSMul (β := LocalizedModule S M) r (mk m s) = mk n t ↔
    mk m s =
      HSMul.hSMul (α := Localization (M := R) S) (β := LocalizedModule S M)
        (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) (mk n t)
Tactic: induction y using induction_on with
    | h n t =>
      rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]
      simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]
      fconstructor
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]
Cleared hypotheses: 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
r : R
hr : r ∈ S
x y : LocalizedModule S M
⊢ r • x = y ↔
    x = HSMul.hSMul (α := Localization (M := R) S) (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) y
have h : ∀ (m : M) (s : ↥S),
  HSMul.hSMul (β := LocalizedModule S M) r (mk m s) = y ↔
    mk m s =
      HSMul.hSMul (α := Localization (M := R) S) (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) y
Tactic: induction x using induction_on with
  | h m s =>
    induction y using induction_on with
    | h n t =>
      rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]
      simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]
      fconstructor
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : r ∈ S
x : LocalizedModule S M
hx : r • x = 0
⊢ x = 0
have hx₁ : x =
  HSMul.hSMul (α := Localization (M := R) S) (β := LocalizedModule S M)
    (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) 0
Tactic: rw [smul_eq_iff_of_mem (hr := hr)] at hx
Cleared hypotheses: hx
-- 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
hr : r ∈ S
x : LocalizedModule S M
hx :
  x =
    HSMul.hSMul (α := Localization (M := R) S) (β := LocalizedModule S M)
      (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) 0
⊢ x = 0
have rw : HSMul.hSMul (α := Localization (M := R) S) (β := LocalizedModule S M)
    (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) 0 =
  0
Tactic: rw [hx, smul_zero]
-- 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
hr : r ∈ S
x : LocalizedModule S M
hx :
  x =
    HSMul.hSMul (α := Localization (M := R) S) (β := LocalizedModule S M)
      (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) 0
rw :
  HSMul.hSMul (α := Localization (M := R) S) (β := LocalizedModule S M)
      (Localization.mk 1 (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr)) 0 =
    0
⊢ x = 0
have rw₁ : Eq (α := LocalizedModule S M) 0 0
Tactic: rw [hx, smul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
p₁ p₂ : LocalizedModule S A
⊢ x • p₁ * p₂ = x • (p₁ * p₂)
have h : ∀ (a₁ s₁ : A) (a₂ s₂ : ↥S),
  HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
Tactic: induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _
Cleared hypotheses: p₁, p₂
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h : HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
  HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
Tactic: rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
⊢ HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₁ : HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
    (mk s₁ s₂) =
  HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
Tactic: rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₁ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
⊢ HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₂ : HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
    (mk s₁ s₂) =
  mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))
Tactic: rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₁ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₂ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))
⊢ HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₃ : Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * a₂ * s₂))
  (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
Tactic: rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₁ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₂ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))
h₃ :
  Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * a₂ * s₂))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
⊢ HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₄ : Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
  (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
Tactic: rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₁ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₂ :
  HMul.hMul (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁) ((IsLocalization.sec S x).2 * a₂))
      (mk s₁ s₂) =
    mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂))
h₃ :
  Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * a₂ * s₂))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
h₄ :
  Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • a₁ * s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
⊢ HSMul.hSMul (β := LocalizedModule S A) x (mk a₁ a₂) * mk s₁ s₂ =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₅ : Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
  (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
Tactic: rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
p₁ p₂ : LocalizedModule S A
⊢ p₁ * x • p₂ = x • (p₁ * p₂)
have h : ∀ (a₁ s₁ : A) (a₂ s₂ : ↥S),
  mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
Tactic: induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _
Cleared hypotheses: p₁, p₂
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h : HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂)
    (mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂)) =
  x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
Tactic: rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂)
      (mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₁ : mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
  x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
Tactic: rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂)
      (mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₁ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₂ : mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
  HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
Tactic: rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂)
      (mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₁ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₂ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₃ : Eq (α := LocalizedModule S A) (mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)))
  (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
Tactic: rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂)
      (mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₁ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₂ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₃ :
  Eq (α := LocalizedModule S A) (mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₄ : Eq (α := LocalizedModule S A) (mk (a₁ * (IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
  (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
Tactic: rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
h :
  HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂)
      (mk ((IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₁ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
h₂ :
  mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)) =
    HSMul.hSMul (β := LocalizedModule S A) x (mk (a₁ * s₁) (a₂ * s₂))
h₃ :
  Eq (α := LocalizedModule S A) (mk (a₁ * (IsLocalization.sec S x).1 • s₁) (a₂ * ((IsLocalization.sec S x).2 * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
h₄ :
  Eq (α := LocalizedModule S A) (mk (a₁ * (IsLocalization.sec S x).1 • s₁) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
    (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
⊢ mk a₁ a₂ * HSMul.hSMul (β := LocalizedModule S A) x (mk s₁ s₂) =
    x • HMul.hMul (α := LocalizedModule S A) (mk a₁ a₂) (mk s₁ s₂)
have h₅ : Eq (α := LocalizedModule S A) (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
  (mk ((IsLocalization.sec S x).1 • (a₁ * s₁)) ((IsLocalization.sec S x).2 * (a₂ * s₂)))
Tactic: rw [smul_def, mk_mul_mk, mk_mul_mk, smul_def, mul_left_comm, mul_smul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
a : R
s : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) 1 = mk ((algebraMap R A : (a : R) → A) a) s
have change : HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) (mk 1 1) = mk ((algebraMap R A : (a : R) → A) a) s
Tactic: change _ • mk _ _ = _
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
T : Type u_1
inst_1 : CommSemiring T
inst_2 : Algebra R T
inst_3 : IsLocalization S T
A : Type u_2
inst_4 : Semiring A
inst_5 : Algebra R A
a : R
s : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S A) (IsLocalization.mk' T a s) (mk 1 1) = mk ((algebraMap R A : (a : R) → A) a) s
have rw : Eq (α := LocalizedModule S A) (mk (HSMul.hSMul (β := A) a 1) (s * 1)) (mk ((algebraMap R A : (a : R) → A) a) s)
Tactic: rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]