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
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ Eq (α := LocalizedModule S M) ((fun (p : Prod.{v, u} M ↥S) ↦ (mk (a.1 • p.1) (a.2 * p.2) : LocalizedModule S M)) p)
    ((fun (p : Prod.{v, u} M ↥S) ↦ (mk (a.1 • p.1) (a.2 * p.2) : LocalizedModule S M)) p')

Tactic:
mk_eq.mpr ⟨s, ?_⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, 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
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x : T
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
refine : s • (a.2 * p'.2) • a.1 • p.1 = s • (a.2 * p.2) • a.1 • p'.1
⊢ Eq (α := LocalizedModule S M) ((fun (p : Prod.{v, u} M ↥S) ↦ (mk (a.1 • p.1) (a.2 * p.2) : LocalizedModule S M)) p)
    ((fun (p : Prod.{v, u} M ↥S) ↦ (mk (a.1 • p.1) (a.2 * p.2) : LocalizedModule S M)) p')

Tactic:
refine mk_eq.mpr ⟨s, ?_⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, 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
T : Type u_1
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalization S T
x : T
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
simp_rw : ((↑s : R) * ((↑a.2 : R) * (↑p'.2 : R) * a.1)) • p.1 = ((↑a.2 : R) * (a.1 * ((↑s : R) * (↑p'.2 : R)))) • p.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1

Tactic:
simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]

Premises used: Submonoid.smul_def, SemigroupAction.mul_smul, 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 : T
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ ((↑s : R) * ((↑a.2 : R) * (↑p'.2 : R) * a.1)) • p.1 = ((↑a.2 : R) * (a.1 * ((↑s : R) * (↑p'.2 : R)))) • p.1

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
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
rw rw₁ : a.2 • a.1 • s • p.2 • p'.1 = a.2 • a.1 • s • p.2 • p'.1
⊢ a.2 • a.1 • s • p'.2 • p.1 = a.2 • a.1 • s • p.2 • p'.1

Tactic:
rw [h]
-- 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
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
simp_rw : ((↑a.2 : R) * (a.1 * ((↑s : R) * (↑p.2 : R)))) • p'.1 = ((↑s : R) * ((↑a.2 : R) * (↑p.2 : R) * a.1)) • p'.1
⊢ a.2 • a.1 • s • p.2 • p'.1 = s • (a.2 * p.2) • a.1 • p'.1

Tactic:
simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]

Premises used: Submonoid.smul_def, SemigroupAction.mul_smul, 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 : T
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
⊢ ((↑a.2 : R) * (a.1 * ((↑s : R) * (↑p.2 : R)))) • p'.1 = ((↑s : R) * ((↑a.2 : R) * (↑p.2 : R) * a.1)) • p'.1

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
p_1 : LocalizedModule S M
a : R × ↥S := IsLocalization.sec S x
p p' : Prod.{v, u} M ↥S
s : ↥S
h : s • p'.2 • p.1 = s • p.2 • p'.1
_ : s • (a.2 * p'.2) • a.1 • p.1 = a.2 • a.1 • s • p'.2 • p.1
_₁ : a.2 • a.1 • s • p'.2 • p.1 = a.2 • a.1 • s • p.2 • p'.1
_₂ : a.2 • a.1 • s • p.2 • p'.1 = s • (a.2 * p.2) • a.1 • p'.1
⊢ s • (a.2 * p'.2) • a.1 • p.1 = s • (a.2 * p.2) • a.1 • p'.1

Tactic:
calc
          _ = a.2 • a.1 • s • p'.2 • p.1 := by
            simp_rw [Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul]; ring_nf
          _ = a.2 • a.1 • s • p.2 • p'.1 := by rw [h]
          _ = s • (a.2 * p.2) • a.1 • p'.1 := by
            simp_rw [Submonoid.smul_def, ← mul_smul, Submonoid.coe_mul]; ring_nf

Premises used: HMul.hMul, Prod.fst, Prod.snd
-- 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
⊢ HSMul.hSMul (β := LocalizedModule S M) x (mk m s) =
    mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s)

Tactic:
rfl

Premises used: LocalizedModule.liftOn, Quotient.mk', OreLocalization.oreDiv, rfl
-- 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
r : R
m : M
s s' : ↥S
rw :
  ∃ (u : ↥S),
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T r s) (mk m s') = mk (r • m) (s * s')

Tactic:
rw [smul_def, mk_eq]

Premises used: LocalizedModule.mk_eq, LocalizedModule.smul_def
-- 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
r : R
m : M
s s' : ↥S
obtain :
  ∀ (c : ↥S)
    (hc :
      (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
        (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)),
    ∃ (u : ↥S),
      u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
        u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
⊢ ∃ (u : ↥S),
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m

Tactic:
obtain ⟨c, hc⟩ := IsLocalization.eq.mp <| IsLocalization.mk'_sec T (IsLocalization.mk' T r s)

Premises used: IsLocalization.mk'_sec, IsLocalization.mk', Iff.mp, IsLocalization.eq
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
⊢ ∃ (u : ↥S),
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m

Tactic:
use c
-- 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
r : R
m : M
s s' c : ↥S
hc :
  (↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    (↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r)
h :
  (c * (s * s')) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) • r • m
h₁ :
  (↑(c * (s * s')) : R) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    (↑(c * ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s')) : R) • r • m
h₂ :
  ((↑c : R) * ((↑s : R) * (↑s' : R))) • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R))) • r • m
h₃ :
  ((↑c : R) * ((↑s : R) * (↑s' : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R)) * r) • m
h₄ :
  ((↑c : R) * (↑s : R) * (↑s' : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑c : R) * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * (↑s' : R) * r) • m
h₅ :
  ((↑s' : R) * ((↑c : R) * (↑s : R)) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) • m =
    ((↑s' : R) * ((↑c : R) * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R)) * r) • m
h₆ :
  ((↑s' : R) * ((↑c : R) * ((↑s : R) * (IsLocalization.sec S (IsLocalization.mk' T r s)).1))) • m =
    ((↑s' : R) * ((↑c : R) * ((↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 : R) * r))) • m
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m

Tactic:
simp_rw [← mul_smul, Submonoid.smul_def, Submonoid.coe_mul, ← mul_smul, ← mul_assoc,
    mul_comm _ (s' : R), mul_assoc, hc]

Premises used: mul_assoc, Submonoid.smul_def, mul_comm, Subtype.val, SemigroupAction.mul_smul, 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
r : R
m : M
s t : ↥S
rw rw₁ : Eq (α := OreLocalization S M) (r • m /ₒ (s * t)) (mk (r • m) (s * t))
⊢ Eq (α := OreLocalization S M) (r • m /ₒ (t * s)) (mk (r • m) (s * t))

Tactic:
rw [mul_comm]

Premises used: 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
p : LocalizedModule S M
h : ∀ (m : M) (s : ↥S), HSMul.hSMul (α := T) (β := LocalizedModule S M) 1 (mk m s) = mk m s
⊢ HSMul.hSMul (α := T) 1 p = 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
m : M
s : ↥S
rw : Eq.{u_1 + 1} (α := T) (1 : T) ((algebraMap R T : (a : R) → T) 1 : T)
rw₁ rw₂ : Eq.{u_1 + 1} (α := T) 1 1
⊢ 1 = IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1

Tactic:
rw [IsLocalization.mk'_one, map_one]

Premises used: map_one, IsLocalization.mk'_one
-- 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 1 1) (mk m s) = mk m s
⊢ HSMul.hSMul (α := T) (β := LocalizedModule S M) 1 (mk m s) = mk m s

Tactic:
rw [show (1 : T) = IsLocalization.mk' T (1 : R) (1 : S) by rw [IsLocalization.mk'_one, map_one]]
-- 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 : Eq (α := LocalizedModule S M) (mk (HSMul.hSMul.{u, v, v} (α := R) 1 m) (1 * s)) (mk m s)
h₁ : Eq (α := LocalizedModule S M) (mk m (1 * s)) (mk m s)
h₂ h₃ : Eq (α := LocalizedModule S M) (mk m s) (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk'.{u, u_1} (R := R) (M := S) T 1 1) (mk m s) = mk m s

Tactic:
rw [mk'_smul_mk, one_smul, one_mul]

Premises used: one_smul, LocalizedModule.mk'_smul_mk, one_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
p : LocalizedModule S M
h :
  ∀ (m : M) (s : ↥S),
    HSMul.hSMul (β := LocalizedModule S M) (x * y) (mk m s) = x • HSMul.hSMul (β := LocalizedModule S M) y (mk m s)
⊢ (x * y) • p = x • 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 :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2)
      (mk m s) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) (mk m s)
⊢ HSMul.hSMul (β := LocalizedModule S M) (x * y) (mk m s) = x • HSMul.hSMul (β := LocalizedModule S M) y (mk m s)

Tactic:
rw [← IsLocalization.mk'_sec (M := S) T x, ← IsLocalization.mk'_sec (M := S) T y]

Premises used: IsLocalization.mk'_sec
-- 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 :
  HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T ((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1)
        ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2))
      (mk m s) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) (mk m s)
h₁ :
  Eq (α := LocalizedModule S M)
    (mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
    (mk ((IsLocalization.sec S x).1 • (IsLocalization.sec S y).1 • m)
      ((IsLocalization.sec S x).2 * ((IsLocalization.sec S y).2 * s)))
h₂ :
  Eq (α := LocalizedModule S M)
    (mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s))
    (mk (((IsLocalization.sec S x).1 * (IsLocalization.sec S y).1) • m)
      ((IsLocalization.sec S x).2 * ((IsLocalization.sec S y).2 * s)))
⊢ HSMul.hSMul (β := LocalizedModule S M)
      (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 *
        IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2)
      (mk m s) =
    IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 •
      HSMul.hSMul (β := LocalizedModule S M)
        (IsLocalization.mk' T (IsLocalization.sec S y).1 (IsLocalization.sec S y).2) (mk m s)

Tactic:
simp_rw [← IsLocalization.mk'_mul, mk'_smul_mk, ← mul_smul, mul_assoc]

Premises used: mul_assoc, LocalizedModule.mk'_smul_mk, SemigroupAction.mul_smul, IsLocalization.mk'_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 : T
p q : LocalizedModule S M
h : ∀ (m : M) (s : ↥S), x • (mk m s + q) = HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + x • q
⊢ x • (p + q) = x • p + x • q

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 : T
q : LocalizedModule S M
m : M
s : ↥S
h :
  ∀ (n : M) (t : ↥S),
    x • HAdd.hAdd (α := LocalizedModule S M) (mk m s) (mk n t) =
      HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + HSMul.hSMul (β := LocalizedModule S M) x (mk n t)
⊢ x • (mk m s + q) = HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + x • q

Tactic:
induction q with | _ n t
-- 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 :
  HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
⊢ x • HAdd.hAdd (α := LocalizedModule S M) (mk m s) (mk n t) =
    HSMul.hSMul (β := LocalizedModule S M) x (mk m s) + HSMul.hSMul (β := LocalizedModule S M) x (mk n t)

Tactic:
rw [smul_def, smul_def, mk_add_mk, mk_add_mk]

Premises used: LocalizedModule.mk_add_mk, LocalizedModule.smul_def
-- 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
rw :
  HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
    HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t))
rw₁ : T
rw₂ :
  HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
    HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t))
rw₃ : T
⊢ HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
    HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk (t • m + s • n) (s * t))

Tactic:
rw [IsLocalization.mk'_sec (M := S) T]

Premises used: IsLocalization.mk'_sec
-- 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 :
  HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk (t • m + s • n) (s * t)) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))
⊢ HSMul.hSMul (β := LocalizedModule S M) x (mk (t • m + s • n) (s * t)) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))

Tactic:
rw [show x • _ = IsLocalization.mk' T _ _ • _ by rw [IsLocalization.mk'_sec (M := S) T]]
-- 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 :
  Eq (α := LocalizedModule S M)
    (mk (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n))
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t)))
    (mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)))
⊢ HSMul.hSMul (β := LocalizedModule S M) (IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2)
      (mk (t • m + s • n) (s * t)) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))

Tactic:
rw [← IsLocalization.mk'_cancel _ _ (IsLocalization.sec S x).2, mk'_smul_mk]

Premises used: IsLocalization.sec, IsLocalization.mk'_cancel, LocalizedModule.mk'_smul_mk, Prod.snd
-- 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 :
  ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n
h₁ :
  (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
⊢ Eq (α := LocalizedModule S M)
    (mk (((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n))
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t)))
    (mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)))

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 : T
m : M
s : ↥S
n : M
t : ↥S
h :
  ((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
⊢ ((IsLocalization.sec S x).1 * (↑(IsLocalization.sec S x).2 : R)) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n

Tactic:
simp only [Submonoid.smul_def, smul_add, ← mul_smul, Submonoid.coe_mul]

Premises used: Submonoid.smul_def, SemigroupAction.mul_smul, smul_add, Submonoid.coe_mul