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
x x_1 x_2 : Prod.{v, u} M ↥S
m1 : M
s1 : ↥S
m2 : M
s2 : ↥S
h_1 : r S M (m1, s1) (m2, s2)
m3 : M
s3 : ↥S
h_2 : r S M (m2, s2) (m3, s3)
u1 : ↥S
hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1
u2 : ↥S
hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1
hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1
hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2
h : (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s3 * (u1 * u2))) • m2
⊢ (s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3
have h₁ : (s2 * (s3 * (u1 * u2))) • m1 = (s2 * (s3 * (u1 * u2))) • m1
Tactic: rw [hu2', hu1']
-- 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
m m' : M
s s' : ↥S
⊢ Eq (α := LocalizedModule S M) (mk m s) (mk m' s') ↔ ∃ (u : ↥S), u • s' • m = u • s • m'
have rw : (∃ (u : ↥S) (v : R), u • m' = v • m ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)) ↔ ∃ (u : ↥S), u • s' • m = u • s • m'
Tactic: rw [mk, mk, OreLocalization.oreDiv_eq_iff]
-- 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
h : 0 ∈ S
⊢ Subsingleton (LocalizedModule S M)
have refine : ∀ (a b : LocalizedModule S M), a = b
Tactic: refine ⟨fun a b ↦ ?_⟩
-- 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
h : 0 ∈ S
a b : LocalizedModule S M
⊢ a = b
have h₁ : ∀ (m m' : M) (s s' : ↥S), Eq (α := LocalizedModule S M) (mk m s) (mk m' s')
Tactic: induction a, b using LocalizedModule.induction_on₂
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ Eq (α := LocalizedModule S A)
    ((fun (x₁ x₂ : Prod.{u_2, u} A ↥S) ↦ (mk (x₁.1 * x₂.1) (x₂.2 * x₁.2) : LocalizedModule S A)) (a₁, s₁) (a₂, s₂))
    ((fun (x₁ x₂ : Prod.{u_2, u} A ↥S) ↦ (mk (x₁.1 * x₂.1) (x₂.2 * x₁.2) : LocalizedModule S A)) (b₁, t₁) (b₂, t₂))
have simp : Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₁ * s₂)) (mk (b₁ * b₂) (t₁ * t₂))
Tactic: simp only [mul_comm s₂ s₁, mul_comm t₂ t₁]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₁ * s₂)) (mk (b₁ * b₂) (t₁ * t₂))
have rw : ∃ (u : ↥S), u • (t₁ * t₂) • (a₁ * a₂) = u • (s₁ * s₂) • (b₁ * b₂)
Tactic: rw [mk_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ ∃ (u : ↥S), u • (t₁ * t₂) • (a₁ * a₂) = u • (s₁ * s₂) • (b₁ * b₂)
have h : (u₁ * u₂) • (t₁ * t₂) • (a₁ * a₂) = (u₁ * u₂) • (s₁ * s₂) • (b₁ * b₂)
Tactic: use u₁ * u₂
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ (u₁ * u₂) • (t₁ * t₂) • (a₁ * a₂) = (u₁ * u₂) • (s₁ * s₂) • (b₁ * b₂)
have h : ((↑u₁ : R) * (↑u₂ : R)) • ((↑t₁ : R) * (↑t₂ : R)) • (a₁ * a₂) =
  ((↑u₁ : R) * (↑u₂ : R)) • ((↑s₁ : R) * (↑s₂ : R)) • (b₁ * b₂)
Tactic: dsimp [Submonoid.smul_def] at *
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂)) *
      Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃) =
    Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁) *
      HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃))
have apply : ∃ (u : ↥S),
  u •
      (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
        (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
    u •
      ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
        ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)
Tactic: apply mk_eq.mpr _
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ ∃ (u : ↥S),
    u •
        (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
          (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
      u •
        ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
          ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)
have h : HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
    ((((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
      (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1)) =
  HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
    (((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
      ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1))
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
⊢ ∀ (a b c : LocalizedModule S A), a * b * c = a * (b * c)
have mk : ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
  (a₃ : A) (s₃ : ↥S),
  HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂)) *
      Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃) =
    Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁) *
      HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃))
Tactic: with_unfolding_all
      rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
      apply mk_eq.mpr _
      use 1
      simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
mk :
  ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
    (a₃ : A) (s₃ : ↥S),
    HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
          (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂)) *
        Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃) =
      Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁) *
        HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂))
          (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃))
⊢ ∀ (a b c : LocalizedModule S A), a * b * c = a * (b * c)
have rintro : ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
  (a₃ : A) (s₃ : ↥S),
  ∃ (u : ↥S),
    u •
        (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
          (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
      u •
        ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
          ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)
Tactic: with_unfolding_all
      rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
      apply mk_eq.mpr _
      use 1
      simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
mk :
  ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
    (a₃ : A) (s₃ : ↥S),
    HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
          (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂)) *
        Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃) =
      Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁) *
        HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂))
          (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃))
rintro :
  ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
    (a₃ : A) (s₃ : ↥S),
    ∃ (u : ↥S),
      u •
          (((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
            (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1) =
        u •
          ((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
            ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1)
⊢ ∀ (a b c : LocalizedModule S A), a * b * c = a * (b * c)
have h : ∀ (a : LocalizedModule S A) (a₁ : A) (s₁ : ↥S) (b : LocalizedModule S A) (a₂ : A) (s₂ : ↥S) (c : LocalizedModule S A)
  (a₃ : A) (s₃ : ↥S),
  HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
      ((((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).2 * (a₁, s₁).2) •
        (((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).1 * (a₃, s₃).1)) =
    HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1
      (((a₃, s₃).2 * ((a₁, s₁).1 * (a₂, s₂).1, (a₂, s₂).2 * (a₁, s₁).2).2) •
        ((a₁, s₁).1 * ((a₂, s₂).1 * (a₃, s₃).1, (a₃, s₃).2 * (a₂, s₂).2).1))
Tactic: with_unfolding_all
      rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨a₃, s₃⟩
      apply mk_eq.mpr _
      use 1
      simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
⊢ HMul.hMul (α := LocalizedModule S A) (mk a₁ s₁) (mk a₂ s₂) = mk (a₁ * a₂) (s₁ * s₂)
have rw : Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₂ * s₁)) (mk (a₁ * a₂) (s₁ * s₂))
Tactic: rw [mk_mul_mk', mul_comm s₁ s₂]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
rw : Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₂ * s₁)) (mk (a₁ * a₂) (s₁ * s₂))
⊢ HMul.hMul (α := LocalizedModule S A) (mk a₁ s₁) (mk a₂ s₂) = mk (a₁ * a₂) (s₁ * s₂)
have rw₁ : Eq (α := LocalizedModule S A) (mk (a₁ * a₂) (s₂ * s₁)) (mk (a₁ * a₂) (s₂ * s₁))
Tactic: rw [mk_mul_mk', mul_comm s₁ s₂]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
⊢ ∀ (a : LocalizedModule S A), 0 * a = 0
have mk : ∀ (a : LocalizedModule S A) (a : A) (s : ↥S),
  HMul.hMul (α := LocalizedModule S A) 0 (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) = 0
Tactic: with_unfolding_all
      rintro ⟨a, s⟩
      exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
⊢ ∀ (a : LocalizedModule S A), a * 0 = 0
have mk : ∀ (a : LocalizedModule S A) (a : A) (s : ↥S),
  HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a, s)) 0 = 0
Tactic: with_unfolding_all
      rintro ⟨a, s⟩
      exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁) *
      HAdd.hAdd (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃)) =
    HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂)) +
      HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃))
have mk : a₁ /ₒ s₁ * HAdd.hAdd (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃) =
  HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) +
    HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃)
Tactic: change a₁ /ₒ s₁ * (a₂ /ₒ s₂ + a₃ /ₒ s₃) = a₁ /ₒ s₁ * (a₂ /ₒ s₂) + a₁ /ₒ s₁ * (a₃ /ₒ s₃)
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ a₁ /ₒ s₁ * HAdd.hAdd (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃) =
    HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) +
      HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃)
have mk : Eq (α := OreLocalization S A) (mk (a₁ * (s₃ • a₂ + s₂ • a₃)) (s₁ * (s₂ * s₃)))
  (mk ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)) (s₁ * s₂ * (s₁ * s₃)))
Tactic: rw [← mk, ← mk, ← mk, mk_mul_mk, mk_mul_mk, mk_add_mk, mk_mul_mk, mk_add_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ Eq (α := OreLocalization S A) (mk (a₁ * (s₃ • a₂ + s₂ • a₃)) (s₁ * (s₂ * s₃)))
    (mk ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)) (s₁ * s₂ * (s₁ * s₃)))
have apply : ∃ (u : ↥S),
  u • (s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃)) =
    u • (s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃))
Tactic: apply mk_eq.mpr _
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ ∃ (u : ↥S),
    u • (s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃)) =
      u • (s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃))
have h : HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * s₂ * (s₁ * s₃)) • (a₁ * (s₃ • a₂ + s₂ • a₃))) =
  HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * (s₂ * s₃)) • ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)))
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ HAdd.hAdd (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂)) *
      Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃) =
    HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₁, s₁))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃)) +
      HMul.hMul (α := LocalizedModule S A) (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₂, s₂))
        (Quot.mk (⇑(OreLocalization.oreEqv S A) : A × ↥S → A × ↥S → Prop) (a₃, s₃))
have mk : HAdd.hAdd (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) * (a₃ /ₒ s₃) =
  HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃) +
    HMul.hMul (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃)
Tactic: change (a₁ /ₒ s₁ + a₂ /ₒ s₂) * (a₃ /ₒ s₃) = a₁ /ₒ s₁ * (a₃ /ₒ s₃) + a₂ /ₒ s₂ * (a₃ /ₒ s₃)
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ HAdd.hAdd (α := OreLocalization S A) (a₁ /ₒ s₁) (a₂ /ₒ s₂) * (a₃ /ₒ s₃) =
    HMul.hMul (α := OreLocalization S A) (a₁ /ₒ s₁) (a₃ /ₒ s₃) +
      HMul.hMul (α := OreLocalization S A) (a₂ /ₒ s₂) (a₃ /ₒ s₃)
have mk : Eq (α := OreLocalization S A) (mk ((s₂ • a₁ + s₁ • a₂) * a₃) (s₁ * s₂ * s₃))
  (mk ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)) (s₁ * s₃ * (s₂ * s₃)))
Tactic: rw [← mk, ← mk, ← mk, mk_mul_mk, mk_mul_mk, mk_add_mk, mk_mul_mk, mk_add_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ Eq (α := OreLocalization S A) (mk ((s₂ • a₁ + s₁ • a₂) * a₃) (s₁ * s₂ * s₃))
    (mk ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)) (s₁ * s₃ * (s₂ * s₃)))
have apply : ∃ (u : ↥S),
  u • (s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃) =
    u • (s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃))
Tactic: apply mk_eq.mpr _
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S_1 : 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_1 T
A : Type u_2
inst_6 : Semiring A
inst_7 : Algebra R A
S : Submonoid R
a : LocalizedModule S A
a₁ : A
s₁ : ↥S
b : LocalizedModule S A
a₂ : A
s₂ : ↥S
c : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ ∃ (u : ↥S),
    u • (s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃) =
      u • (s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃))
have h : HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * s₃ * (s₂ * s₃)) • ((s₂ • a₁ + s₁ • a₂) * a₃)) =
  HSMul.hSMul.{u, u_2, u_2} (α := ↥S) 1 ((s₁ * s₂ * s₃) • ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)))
Tactic: use 1