awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
s : ↥S
rw : mk' f (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M) 0 0) s = 0
rw₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 (mk' f 0 s) = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M') 0 0
⊢ mk' f 0 s = 0

Tactic:
rw [← zero_smul R (0 : M), mk'_smul, zero_smul]

Premises used: zero_smul, IsLocalizedModule.mk'_smul, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
delta :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
⊢ mk' (S := S) f m 1 = (f : (a : M) → M') m

Tactic:
delta mk'

Premises used: IsLocalizedModule.mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
rw :
  Eq (α := M')
    (((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
        ((f : (a : M) → M') m : M') :
      M')
    ((f : (a : M) → M') m : M')
rw₁ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') (↑1 : R) ((f : (a : M) → M') m : M')
rw₂ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') 1 ((f : (a : M) → M') m : M')
rw₃ rw₄ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') ((f : (a : M) → M') m : M')
⊢ Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')

Tactic:
rw [fromLocalizedModule_mk, Module.End.algebraMap_isUnit_inv_apply_eq_iff, Submonoid.coe_one,
    one_smul]

Premises used: IsLocalizedModule.fromLocalizedModule_mk, one_smul, Submonoid.coe_one, Module.End.algebraMap_isUnit_inv_apply_eq_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
delta :
  Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')
⊢ mk' f (s • m) s = (f : (a : M) → M') m

Tactic:
delta mk'

Premises used: IsLocalizedModule.mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
rw :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) : M')
    ((f : (a : M) → M') m : M')
rw₁ : (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m 1) = mk' (S := S) f m 1
rw₂ :
  ((↑(IsUnit.unit (a := (algebraMap R (End R M') : (a : R) → End R M') (↑1 : R)) ⋯)⁻¹ : End R M') : (a : M') → M')
      ((f : (a : M) → M') m : M') =
    mk' (S := S) f m 1
rw₃ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (↑1 : R) (mk' (S := S) f m 1)
rw₄ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) 1 (mk' (S := S) f m 1)
rw₅ : (f : (a : M) → M') m = HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M') 1 ((f : (a : M) → M') m : M')
rw₆ rw₇ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') ((f : (a : M) → M') m : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s • m) s) : M')
    ((f : (a : M) → M') m : M')

Tactic:
rw [LocalizedModule.mk_cancel, ← mk'_one S f, fromLocalizedModule_mk,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff, OneMemClass.coe_one, mk'_one, one_smul]

Premises used: OneMemClass.coe_one, LocalizedModule.mk_cancel, IsLocalizedModule.fromLocalizedModule_mk, IsLocalizedModule.mk'_one, one_smul, Module.End.algebraMap_isUnit_inv_apply_eq_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
rw : (↑s : R) • mk' f m s = (f : (a : M) → M') m
rw₁ : mk' f ((↑s : R) • m) s = (f : (a : M) → M') m
rw₂ : mk' f (s • m) s = (f : (a : M) → M') m
rw₃ rw₄ : Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') ((f : (a : M) → M') m : M')
⊢ s • mk' f m s = (f : (a : M) → M') m

Tactic:
rw [Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]

Premises used: Submonoid.smul_def, IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_cancel
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
delta :
  Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')
⊢ mk' f (s₁ • m) (s₁ * s₂) = mk' f m s₂

Tactic:
delta mk'

Premises used: IsLocalizedModule.mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
rw rw₁ :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₁ • m) (s₁ * s₂)) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₂) : M')

Tactic:
rw [LocalizedModule.mk_cancel_common_left]

Premises used: LocalizedModule.mk_cancel_common_left
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
delta :
  Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')
⊢ mk' f (s₂ • m) (s₁ * s₂) = mk' f m s₁

Tactic:
delta mk'

Premises used: IsLocalizedModule.mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s₁ s₂ : ↥S
rw rw₁ :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')
⊢ Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m) (s₁ * s₂)) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s₁) : M')

Tactic:
rw [LocalizedModule.mk_cancel_common_right]

Premises used: LocalizedModule.mk_cancel_common_right
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
rw : mk' f (m₁ + m₂) s = mk' f (s • m₁ + s • m₂) (s * s)
rw₁ : mk' f (m₁ + m₂) s = mk' f (s • (m₁ + m₂)) (s * s)
rw₂ rw₃ : mk' f (m₁ + m₂) s = mk' f (m₁ + m₂) s
⊢ mk' f (m₁ + m₂) s = mk' f m₁ s + mk' f m₂ s

Tactic:
rw [mk'_add_mk', ← smul_add, mk'_cancel_left]

Premises used: IsLocalizedModule.mk'_add_mk', smul_add, IsLocalizedModule.mk'_cancel_left
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
delta :
  Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₁ s₁) : M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₂ s₂) : M') ↔
    ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁
⊢ mk' f m₁ s₁ = mk' f m₂ s₂ ↔ ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁

Tactic:
delta mk'

Premises used: IsLocalizedModule.mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
rw : (∃ (u : ↥S), u • s₂ • m₁ = u • s₁ • m₂) ↔ ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁
⊢ Eq.{u_3 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₁ s₁) : M')
      ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m₂ s₂) : M') ↔
    ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁

Tactic:
rw [(fromLocalizedModule.inj S f).eq_iff, LocalizedModule.mk_eq]

Premises used: LocalizedModule.mk_eq, Function.Injective.eq_iff, IsLocalizedModule.fromLocalizedModule.inj
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (∃ (u : ↥S), u • s₂ • m₁ = u • s₁ • m₂) ↔ ∃ (s : ↥S), s • s₁ • m₂ = s • s₂ • m₁

Tactic:
simp_rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
delta :
  Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (-m) s) : M')
    (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
⊢ mk' f (-m) s = -mk' f m s

Tactic:
delta mk'

Premises used: IsLocalizedModule.mk'
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
rw :
  Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (-LocalizedModule.mk m s) : M')
    (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
rw₁ rw₂ :
  Eq.{u_7 + 1} (α := M') (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
    (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
⊢ Eq.{u_7 + 1} (α := M') ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (-m) s) : M')
    (-(fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')

Tactic:
rw [LocalizedModule.mk_neg, map_neg]

Premises used: map_neg, LocalizedModule.mk_neg
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
rw : mk' f (m₁ + -m₂) s = mk' f m₁ s - mk' f m₂ s
rw₁ : mk' f (m₁ + -m₂) s = mk' f m₁ s + -mk' f m₂ s
rw₂ : mk' f m₁ s + mk' f (-m₂) s = mk' f m₁ s + -mk' f m₂ s
rw₃ rw₄ : mk' f m₁ s + -mk' f m₂ s = mk' f m₁ s + -mk' f m₂ s
⊢ mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, mk'_add, mk'_neg]

Premises used: sub_eq_add_neg, IsLocalizedModule.mk'_add, IsLocalizedModule.mk'_neg
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : AddCommGroup M
inst_2 : SubtractionCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
rw : mk' f m₁ s₁ + -mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₁ : mk' f m₁ s₁ + mk' f (-m₂) s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₂ : mk' f (s₂ • m₁ + s₁ • -m₂) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₃ : mk' f (s₂ • m₁ + -(s₁ • m₂)) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
rw₄ rw₅ : mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂) = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)

Tactic:
rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]

Premises used: IsLocalizedModule.mk'_add_mk', sub_eq_add_neg, smul_neg, IsLocalizedModule.mk'_neg
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
symm : mk' f (m₁ * m₂) (s₁ * s₂) = mk' f m₁ s₁ * mk' f m₂ s₂
⊢ mk' f m₁ s₁ * mk' f m₂ s₂ = mk' f (m₁ * m₂) (s₁ * s₂)

Tactic:
symm
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
apply : (f : (a : M) → M') (m₁ * m₂, s₁ * s₂).1 = (↑(m₁ * m₂, s₁ * s₂).2 : R) • (mk' f m₁ s₁ * mk' f m₂ s₂)
⊢ mk' f (m₁ * m₂) (s₁ * s₂) = mk' f m₁ s₁ * mk' f m₂ s₂

Tactic:
apply (Module.End.algebraMap_isUnit_inv_apply_eq_iff _ _ _ _).mpr

Premises used: Iff.mpr, Module.End.algebraMap_isUnit_inv_apply_eq_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
simp_rw : (f : (a : M) → M') (m₁ • m₂) = ((↑s₁ : R) • (↑s₂ : R)) • mk' f m₁ s₁ • mk' f m₂ s₂
⊢ (f : (a : M) → M') (m₁ * m₂, s₁ * s₂).1 = (↑(m₁ * m₂, s₁ * s₂).2 : R) • (mk' f m₁ s₁ * mk' f m₂ s₂)

Tactic:
simp_rw [Submonoid.coe_mul, ← smul_eq_mul]

Premises used: smul_eq_mul, Submonoid.coe_mul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
rw : (f : (a : M) → M') (m₁ • m₂) = mk' f ((↑s₁ : R) • m₁) s₁ • mk' f ((↑s₂ : R) • m₂) s₂
⊢ (f : (a : M) → M') (m₁ • m₂) = ((↑s₁ : R) • (↑s₂ : R)) • mk' f m₁ s₁ • mk' f m₂ s₂

Tactic:
rw [smul_smul_smul_comm, ← mk'_smul, ← mk'_smul]

Premises used: smul_smul_smul_comm, IsLocalizedModule.mk'_smul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : NonUnitalNonAssocSemiring M
inst_2 : Semiring M'
inst_3 : Module R M
inst_4 : Algebra R M'
f : M →ₗ[R] M'
hf :
  ∀ (m₁ m₂ : M),
    (f : (a : M) → M') (m₁ * m₂) =
      HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
inst_5 : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
simp_rw : (f : (a : M) → M') (m₁ • m₂) = mk' f (s₁ • m₁) s₁ • mk' f (s₂ • m₂) s₂
simp_rw₁ :
  (f : (a : M) → M') (m₁ • m₂) =
    HSMul.hSMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
simp_rw₂ :
  (f : (a : M) → M') (m₁ * m₂) = HMul.hMul (α := M') (β := M') ((f : (a : M) → M') m₁ : M') ((f : (a : M) → M') m₂ : M')
⊢ (f : (a : M) → M') (m₁ • m₂) = mk' f ((↑s₁ : R) • m₁) s₁ • mk' f ((↑s₂ : R) • m₂) s₂

Tactic:
simp_rw [← Submonoid.smul_def, mk'_cancel, smul_eq_mul, hf]

Premises used: Submonoid.smul_def, smul_eq_mul, IsLocalizedModule.mk'_cancel
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst_1 : Semiring M
inst_2 : Semiring M'
inst_3 : Algebra R M
inst_4 : Algebra R M'
f : M →ₐ[R] M'
inst_5 : IsLocalizedModule S f.toLinearMap
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f.toLinearMap m₁ s₁ * mk' f.toLinearMap m₂ s₂ = mk' f.toLinearMap (m₁ * m₂) (s₁ * s₂)

Tactic:
mk'_mul_mk'_of_map_mul f.toLinearMap (map_mul f) m₁ m₂ s₁ s₂

Premises used: AlgHom.toLinearMap, map_mul, IsLocalizedModule.mk'_mul_mk'_of_map_mul
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
m' : M'
rw : s • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₁ : (↑s : R) • mk' f m s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₂ : mk' f ((↑s : R) • m) s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₃ : mk' f (s • m) s = s • m' ↔ (f : (a : M) → M') m = s • m'
rw₄ rw₅ : (f : (a : M) → M') m = s • m' ↔ (f : (a : M) → M') m = s • m'
⊢ mk' f m s = m' ↔ (f : (a : M) → M') m = s • m'

Tactic:
rw [← smul_inj f s, Submonoid.smul_def, ← mk'_smul, ← Submonoid.smul_def, mk'_cancel]

Premises used: Submonoid.smul_def, IsLocalizedModule.smul_inj, IsLocalizedModule.mk'_smul, IsLocalizedModule.mk'_cancel
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
rw : (f : (a : M) → M') m = HSMul.hSMul (β := M') s 0 ↔ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M') ↔
    Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')
⊢ mk' f m s = 0 ↔ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') m : M') (0 : M')

Tactic:
rw [mk'_eq_iff, smul_zero]

Premises used: smul_zero, IsLocalizedModule.mk'_eq_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M
s : ↥S
simp_rw : mk' f m s = mk' (S := S) f 0 1 ↔ ∃ (s' : ↥S), s' • m = 0
simp_rw₁ :
  (∃ (s_1 : ↥S), s_1 • HSMul.hSMul (β := M) s 0 = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 m) ↔
    ∃ (s' : ↥S), s' • m = 0
simp_rw₂ : (∃ (s : ↥S), 0 = s • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 m) ↔ ∃ (s' : ↥S), s' • m = 0
simp_rw₃ : (∃ (s : ↥S), 0 = s • m) ↔ ∃ (s' : ↥S), s' • m = 0
⊢ mk' f m s = 0 ↔ ∃ (s' : ↥S), s' • m = 0

Tactic:
simp_rw [← mk'_zero f (1 : S), mk'_eq_mk'_iff, smul_zero, one_smul, eq_comm]

Premises used: IsLocalizedModule.mk'_zero, IsLocalizedModule.mk'_eq_mk'_iff, smul_zero, eq_comm, one_smul, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : ↥S
m : M
rw : Eq (α := LocalizedModule S M) (mk' (LocalizedModule.mkLinearMap S M) m s) (LocalizedModule.mk m s)
rw₁ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) s (LocalizedModule.mk m s)
rw₂ :
  (LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m =
    HSMul.hSMul (β := LocalizedModule S M) (↑s : R) (LocalizedModule.mk m s)
rw₃ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk ((↑s : R) • m) s : LocalizedModule S M)
rw₄ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk (s • m) s : LocalizedModule S M)
rw₅ :
  Eq (α := LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk m 1 : LocalizedModule S M)
rw₆ rw₇ : Eq (α := LocalizedModule S M) (LocalizedModule.mk m 1) (LocalizedModule.mk m 1)
⊢ Eq (α := LocalizedModule S M) (LocalizedModule.mk m s) (mk' (LocalizedModule.mkLinearMap S M) m s)

Tactic:
rw [eq_comm, mk'_eq_iff, Submonoid.smul_def, LocalizedModule.smul'_mk, ← Submonoid.smul_def,
    LocalizedModule.mk_cancel, LocalizedModule.mkLinearMap_apply]

Premises used: LocalizedModule.mk_cancel, LocalizedModule.smul'_mk, eq_comm, Submonoid.smul_def, LocalizedModule.mkLinearMap_apply, IsLocalizedModule.mk'_eq_iff
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
a :
  Eq.{u_3 + 1} (α := M') ((fun (m : M') ↦ (s * t) • m) (IsLocalization.mk' A x s • mk' f m t))
    ((fun (m : M') ↦ (s * t) • m) (mk' f (x • m) (s * t)))
⊢ IsLocalization.mk' A x s • mk' f m t = mk' f (x • m) (s * t)

Tactic:
apply smul_injective f (s * t)

Premises used: HMul.hMul, IsLocalizedModule.smul_injective
-- Module: Mathlib.Algebra.Module.LocalizedModule.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
A : Type u_5
inst_3 : CommSemiring A
inst_4 : Algebra R A
inst_5 : Module A M'
inst_6 : IsLocalization S A
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : IsScalarTower R A M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
x : R
m : M
s t : ↥S
simp : s • IsLocalization.mk' A x s • t • mk' f m t
| (fun (m : M') ↦ (s * t) • m) (IsLocalization.mk' A x s • mk' f m t)

Tactic:
simp only [smul_assoc, mul_smul, smul_comm t]

Premises used: smul_assoc, SMulCommClass.smul_comm, SemigroupAction.mul_smul