awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R) * (↑t : R)) • m +
      ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R) * (↑s : R)) • n =
    ((↑(IsLocalization.sec S x).2 : R) * (↑t : R) * (IsLocalization.sec S x).1) • m +
      ((↑(IsLocalization.sec S x).2 : R) * (↑s : R) * (IsLocalization.sec S x).1) • n

Tactic:
ring_nf
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
m : M
s : ↥S
n : M
t : ↥S
h h₁ :
  (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)

Tactic:
rw [mul_mul_mul_comm]

Premises used: mul_mul_mul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
lhs : HSMul.hSMul (β := LocalizedModule S M) x 0
| HSMul.hSMul (β := LocalizedModule S M) x 0 = 0

Tactic:
lhs
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
rw : 0
| HSMul.hSMul (β := LocalizedModule S M) x 0

Tactic:
rw [← zero_mk 1, smul_def, smul_zero, zero_mk]

Premises used: smul_zero, LocalizedModule.smul_def, OfNat.ofNat, LocalizedModule.zero_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
rw : 0
| HSMul.hSMul (β := LocalizedModule S M) x 0 = 0

Tactic:
lhs; rw [← zero_mk 1, smul_def, smul_zero, zero_mk]

Premises used: smul_zero, LocalizedModule.smul_def, OfNat.ofNat, LocalizedModule.zero_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
conv : HSMul.hSMul (β := LocalizedModule S M) x 0 = 0
conv₁ : Eq (α := LocalizedModule S M) 0 0
⊢ HSMul.hSMul (β := LocalizedModule S M) x 0 = 0

Tactic:
conv => lhs; rw [← zero_mk 1, smul_def, smul_zero, zero_mk]

Premises used: smul_zero, LocalizedModule.smul_def, OfNat.ofNat, LocalizedModule.zero_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
h :
  ∀ (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)
⊢ (x + y) • p = x • p + y • p

Tactic:
induction p with | _ m s
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 :
  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)))
⊢ 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)

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]

Premises used: LocalizedModule.mk_add_mk, smul_assoc, LocalizedModule.smul_def, add_smul, LocalizedModule.mk'_smul_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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)
⊢ 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:
congr 1
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 : R) * (↑s : R) * (IsLocalization.sec S x).1 +
        (↑(IsLocalization.sec S x).2 : R) * (↑s : R) * (IsLocalization.sec S y).1) •
      m
⊢ (((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:
simp only [Submonoid.smul_def, Submonoid.coe_mul, smul_eq_mul]

Premises used: Submonoid.smul_def, smul_eq_mul, Submonoid.coe_mul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 : R) * (↑s : R) * (IsLocalization.sec S x).1 +
        (↑(IsLocalization.sec S x).2 : R) * (↑s : R) * (IsLocalization.sec S y).1) •
      m

Tactic:
ring_nf
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)
h₁ 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)

Tactic:
rw [mul_mul_mul_comm, mul_assoc]

Premises used: mul_mul_mul_comm, mul_assoc
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
h : ∀ (m : M) (s : ↥S), HSMul.hSMul (α := T) (β := LocalizedModule S M) 0 (mk m s) = 0
⊢ HSMul.hSMul (α := T) 0 p = 0

Tactic:
induction p with | _ m s
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 rw₁ : Eq.{u_1 + 1} (α := T) 0 0
⊢ 0 = IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 0 1

Tactic:
rw [IsLocalization.mk'_zero]

Premises used: IsLocalization.mk'_zero
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
h₃ h₄ : Eq (α := LocalizedModule S M) 0 0
⊢ HSMul.hSMul (α := T) (β := LocalizedModule S M) 0 (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]

Premises used: zero_smul, LocalizedModule.mk'_smul_mk, LocalizedModule.zero_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
simp : s • s' • m = s' • s • m
⊢ HSMul.hSMul.{u, v, v} (α := ↥S) 1 (s • s' • m) = HSMul.hSMul.{u, v, v} (α := ↥S) 1 ((s' * s) • m)

Tactic:
simp only [mul_smul, one_smul]

Premises used: one_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
rw rw₁ : s' • s • m = s' • s • m
⊢ s • s' • m = s' • s • m

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u
inst : CommSemiring R
S : Submonoid R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
⊢ HSMul.hSMul.{u, v, v} (α := ↥S) 1 (HSMul.hSMul.{u, v, v} (α := ↥S) 1 (s • m)) =
    HSMul.hSMul.{u, v, v} (α := ↥S) 1 (s • m)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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)

Tactic:
simp [mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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

Tactic:
(OreLocalization.smul_oreDiv _ _ _).trans ?_

Premises used: OreLocalization.smul_oreDiv, Eq.trans
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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)
⊢ HSMul.hSMul (β := LocalizedModule S M) r (mk m s) = mk (r • m) s

Tactic:
refine (OreLocalization.smul_oreDiv _ _ _).trans ?_

Premises used: OreLocalization.smul_oreDiv, Eq.trans
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
⊢ 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:
simp
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 :
  (∃ (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
⊢ 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:
rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]

Premises used: LocalizedModule.mk_eq, LocalizedModule.smul'_mk, one_smul, LocalizedModule.mk_smul_mk
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
⊢ (∃ (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:
simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]

Premises used: Subtype.exists, Submonoid.mk_smul, exists_prop
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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
⊢ (∃ 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
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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

Tactic:
⟨a, ha, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 ∈ S, a • (Subtype.mk (p := fun (x : R) ↦ x ∈ S) r hr * t) • m = a • s • n

Tactic:
refine ⟨a, ha, ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
h₃ h₄ : a • t • r • m = a • t • r • m
⊢ 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]

Premises used: Submonoid.mk_smul, SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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

Tactic:
⟨a, ha, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 • s • n
⊢ ∃ a ∈ S, a • t • r • m = a • s • n

Tactic:
refine ⟨a, ha, ?_⟩
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
h₅ h₆ : a • (↑t : R) • r • m = a • (↑t : R) • r • m
⊢ a • t • r • m = a • s • n

Tactic:
rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]

Premises used: Submonoid.mk_smul, Submonoid.smul_def, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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)
⊢ 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 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]

Premises used: LocalizedModule.mk_eq, Subtype.exists, Submonoid.mk_smul, exists_prop, LocalizedModule.smul'_mk, one_smul, Submonoid.smul_def, mul_comm, LocalizedModule.mk_smul_mk, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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
⊢ r • x = y ↔
    x = 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]

Premises used: LocalizedModule.mk_eq, Subtype.exists, Submonoid.mk_smul, exists_prop, LocalizedModule.smul'_mk, one_smul, Submonoid.smul_def, mul_comm, LocalizedModule.mk_smul_mk, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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 =
    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

Premises used: LocalizedModule.smul_eq_iff_of_mem
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
rw₁ rw₂ : Eq (α := LocalizedModule S M) 0 0
⊢ x = 0

Tactic:
rw [hx, smul_zero]

Premises used: smul_zero
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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₂)

Tactic:
_
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
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
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₂)
⊢ x • p₁ * p₂ = x • (p₁ * p₂)

Tactic:
induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _