awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x y : T
m : M
s : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 +
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2)
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₂ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (x + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
have rw₃ : HSMul.hSMul (β := LocalizedModule S M)
    (IsLocalization.mk' T
      ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
        (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
    (mk m s) =
  HSMul.hSMul (β := LocalizedModule S M)
    (IsLocalization.mk' T
      ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
        (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
    (mk m s)
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x y : T
m : M
s : ↥S
rw :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₁ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 +
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2)
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₂ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
rw₃ :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (x + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T
        (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R))
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
      (mk m s)
have rw₄ : R
Tactic: rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ HSMul.hSMul (β := LocalizedModule S M) (x + y) (mk m s) =
    HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + HSMul.hSMul (β := LocalizedModule S M) y (mk m s)
have h : Eq (α := LocalizedModule S M)
  (mk
    ((((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
        (↑s : R)) •
      m)
    ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s))
  (mk
    ((((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m)
    ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)))
Tactic: rw [smul_def T x, smul_def T y, mk_add_mk, show (x + y) • _ = IsLocalization.mk' T _ _ • _ by
    rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y,
      ← IsLocalization.mk'_add, IsLocalization.mk'_cancel _ _ s], mk'_smul_mk, ← smul_assoc,
    ← smul_assoc, ← add_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 y : T
m : M
s : ↥S
⊢ Eq (α := LocalizedModule S M)
    (mk
      ((((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R)) •
        m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s))
    (mk
      ((((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
          ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
        m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)))
have h : (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
        (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
      (↑s : R)) •
    m =
  (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
    m
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x y : T
m : M
s : ↥S
h :
  (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
        (↑s : R)) •
      m =
    (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m
⊢ Eq (α := LocalizedModule S M)
    (mk
      ((((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
            (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
          (↑s : R)) •
        m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s))
    (mk
      ((((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
          ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
        m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)))
have h₁ : (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
  (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
          (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
        (↑s : R)) •
      m =
    (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m
have h : (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S y).2 : R) +
        (IsLocalization.sec S y).1 * (↑(IsLocalization.sec S x).2 : R)) *
      (↑s : R)) •
    m =
  ((↑(IsLocalization.sec S y).2 : R) * (↑s : R) * (IsLocalization.sec S x).1 +
      (↑(IsLocalization.sec S x).2 : R) * (↑s : R) * (IsLocalization.sec S y).1) •
    m
Tactic: simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_eq_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
m : M
s : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)
have h : (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
  (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * (s * s)
Tactic: rw [mul_mul_mul_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x y : T
m : M
s : ↥S
h :
  (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * (s * s)
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)
have h₁ : (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * (s * s) =
  (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * (s * s)
Tactic: rw [mul_mul_mul_comm, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
p : LocalizedModule S M
⊢ HSMul.hSMul (α := T) 0 p = 0
have h : ∀ (m : M) (s : ↥S), HSMul.hSMul (α := T) (β := LocalizedModule S M) 0 (mk m s) = 0
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
⊢ 0 = IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 0 1
have rw : Eq.{u_1 + 1} (α := T) 0 0
Tactic: rw [IsLocalization.mk'_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
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) 0 (mk m s) = 0
have h : HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 0 1) (mk m s) = 0
Tactic: rw [show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],
    mk'_smul_mk, zero_smul, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
m : M
s : ↥S
h : HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 0 1) (mk m s) = 0
⊢ HSMul.hSMul (α := T) (β := LocalizedModule S M) 0 (mk m s) = 0
have h₁ : Eq (α := LocalizedModule S M) (mk (HSMul.hSMul.{u, v, v} (α := R) 0 m) (1 * s)) 0
Tactic: rw [show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],
    mk'_smul_mk, zero_smul, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
m : M
s : ↥S
h : HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 0 1) (mk m s) = 0
h₁ : Eq (α := LocalizedModule S M) (mk (HSMul.hSMul.{u, v, v} (α := R) 0 m) (1 * s)) 0
⊢ HSMul.hSMul (α := T) (β := LocalizedModule S M) 0 (mk m s) = 0
have h₂ : Eq (α := LocalizedModule S M) (mk 0 (1 * s)) 0
Tactic: rw [show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],
    mk'_smul_mk, zero_smul, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
m : M
s : ↥S
h : HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 0 1) (mk m s) = 0
h₁ : Eq (α := LocalizedModule S M) (mk (HSMul.hSMul.{u, v, v} (α := R) 0 m) (1 * s)) 0
h₂ : Eq (α := LocalizedModule S M) (mk 0 (1 * s)) 0
⊢ HSMul.hSMul (α := T) (β := LocalizedModule S M) 0 (mk m s) = 0
have h₃ : Eq (α := LocalizedModule S M) 0 0
Tactic: rw [show (0 : T) = IsLocalization.mk' T (0 : R) (1 : S) by rw [IsLocalization.mk'_zero],
    mk'_smul_mk, zero_smul, zero_mk]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s' s : ↥S
m : M
⊢ HSMul.hSMul.{u, v, v} (α := ↥S) 1 (s • s' • m) = HSMul.hSMul.{u, v, v} (α := ↥S) 1 ((s' * s) • m)
have simp : s • s' • m = s' • s • m
Tactic: simp only [mul_smul, one_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
s' s : ↥S
m : M
⊢ s • s' • m = s' • s • m
have rw : s' • s • m = s' • s • m
Tactic: rw [smul_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
r : R
s : ↥S
m : M
⊢ HSMul.hSMul (β := LocalizedModule S M) r (mk m s) = mk (r • m) s
have refine : Eq (α := OreLocalization S M)
  (OreLocalization.oreNum (HSMul.hSMul (β := R) r 1) s • m /ₒ OreLocalization.oreDenom (HSMul.hSMul (β := R) r 1) s)
  (mk (r • m) s)
Tactic: refine (OreLocalization.smul_oreDiv _ _ _).trans ?_
-- 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
⊢ 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)
have h : (∃ (u : ↥S), u • t • r • m = u • s • n) ↔
  ∃ (u : ↥S), u • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = u • s • n
Tactic: rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, 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
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ (∃ (u : ↥S), u • t • r • m = u • s • n) ↔
    ∃ (u : ↥S), u • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = u • s • n
have h : (∃ a ∈ S, a • t • r • m = a • s • n) ↔ ∃ a ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
Tactic: simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]
-- 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 ∈ S, a • t • r • m = a • s • n) ↔ ∃ a ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
have h : (∃ a ∈ S, a • t • r • m = a • s • n) → ∃ a ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
Tactic: fconstructor
-- 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
h : (∃ a ∈ S, a • t • r • m = a • s • n) → ∃ a ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
⊢ (∃ a ∈ S, a • t • r • m = a • s • n) ↔ ∃ a ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
have h₁ : (∃ a ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n) → ∃ a ∈ S, a • t • r • m = a • s • n
Tactic: fconstructor
-- 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 • t • r • m = a • s • n
⊢ ∃ a ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
have h : a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
Tactic: refine ⟨a, ha, ?_⟩
-- 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 • t • r • m = a • s • n
⊢ a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
have h : a • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • t • m = a • s • n
Tactic: rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
h : a • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • t • m = a • s • n
⊢ a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
have h₁ : a • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • t • m = a • t • r • m
Tactic: rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
h : a • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • t • m = a • s • n
h₁ : a • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • t • m = a • t • r • m
⊢ a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
have h₂ : a • r • t • m = a • t • r • m
Tactic: rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
a : R
ha : a ∈ S
eq1 : a • t • r • m = a • s • n
h : a • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • t • m = a • s • n
h₁ : a • Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr • t • m = a • t • r • m
h₂ : a • r • t • m = a • t • r • m
⊢ a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n
have h₃ : a • t • r • m = a • t • r • m
Tactic: rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
-- Lean 4 proof step from Mathlib.Algebra.Module.LocalizedModule.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
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
⊢ ∃ a ∈ S, a • t • r • m = a • s • n
have h : a • t • r • m = a • s • n
Tactic: refine ⟨a, ha, ?_⟩
-- 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
⊢ a • t • r • m = a • s • n
have h : a • t • r • m = a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • 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
⊢ 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]