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
m : M'
apply_fun :
  Eq.{u_3 + 1} (α := M')
    ((iso S f : (a : LocalizedModule S M) → M')
        (((iso S f).symm : (a : M') → LocalizedModule S M) m : LocalizedModule S M) :
      M')
    ((iso S f : (a : LocalizedModule S M) → M')
        (LocalizedModule.mk ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
          ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2) :
      M')
⊢ Eq (α := LocalizedModule S M) (((iso S f).symm : (a : M') → LocalizedModule S M) m : LocalizedModule S M)
    (LocalizedModule.mk ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
        ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2 :
      LocalizedModule S M)

Tactic:
apply_fun iso S f using LinearEquiv.injective (iso S f)

Premises used: IsLocalizedModule.iso, LinearEquiv.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'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M'
rw :
  m =
    (iso S f : (a : LocalizedModule S M) → M')
      (LocalizedModule.mk ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
        ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2)
⊢ Eq.{u_3 + 1} (α := M')
    ((iso S f : (a : LocalizedModule S M) → M')
        (((iso S f).symm : (a : M') → LocalizedModule S M) m : LocalizedModule S M) :
      M')
    ((iso S f : (a : LocalizedModule S M) → M')
        (LocalizedModule.mk ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
          ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2) :
      M')

Tactic:
rw [LinearEquiv.apply_symm_apply]

Premises used: LinearEquiv.apply_symm_apply
-- 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 =
    (iso S f : (a : LocalizedModule S M) → M')
      (LocalizedModule.mk ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).1
        ⋯.choose (p := fun (x : Prod.{u_2, u_1} M ↥S) ↦ x.2 • m = (f : (a : M) → M') x.1).2)

Tactic:
simp [iso, fromLocalizedModule, Module.End.algebraMap_isUnit_inv_apply_eq_iff',
    ← Submonoid.smul_def, (surj _ _ _).choose_spec]

Premises used: Exists.choose_spec, IsLocalizedModule.iso, Module.End.algebraMap_isUnit_inv_apply_eq_iff', Submonoid.smul_def, IsLocalizedModule.fromLocalizedModule, IsLocalizedModule.surj
-- 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
h :
  ∀ (m : M),
    Eq (α := LocalizedModule S M)
      (((↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
      ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
⊢ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f = LocalizedModule.mkLinearMap S M

Tactic:
ext m
-- 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
h : HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := M') 1 ((f : (a : M) → M') m : M') = (f : (a : M) → M') m
⊢ Eq (α := LocalizedModule S M)
    (((↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f : (a : M) → LocalizedModule S M) m : LocalizedModule S M)
    ((LocalizedModule.mkLinearMap S M : (a : M) → LocalizedModule S M) m : LocalizedModule S M)

Tactic:
rw [LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.coe_coe, iso_symm_apply']

Premises used: IsLocalizedModule.iso_symm_apply', LinearMap.comp_apply, LocalizedModule.mkLinearMap_apply, LinearEquiv.coe_coe
-- 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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := M') 1 ((f : (a : M) → M') m : M') = (f : (a : M) → M') m

Tactic:
one_smul _ _

Premises used: one_smul
-- 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
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := ↥S) (β := M') 1 ((f : (a : M) → M') m : M') = (f : (a : M) → M') m

Tactic:
exact one_smul _ _

Premises used: one_smul
-- 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
x : M
⊢ Eq (α := LocalizedModule S M)
    (((iso S f).symm : (a : M') → LocalizedModule S M) ((f : (a : M) → M') x) : LocalizedModule S M)
    (LocalizedModule.mk x 1 : LocalizedModule S M)

Tactic:
DFunLike.congr_fun (iso_symm_comp S f) x

Premises used: DFunLike.congr_fun, IsLocalizedModule.iso_symm_comp, Function.surjInv, Quotient.mk', Classical.choose, OreLocalization.oreDiv
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
rw : LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) ∘ₗ f = g
rw₁ : LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap S M = g
rw₂ rw₃ : g = g
⊢ (LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M)) ∘ₗ f = g

Tactic:
rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]

Premises used: LinearMap.comp_assoc, IsLocalizedModule.iso_symm_comp, LocalizedModule.lift_comp
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst_7 : IsLocalizedModule S f
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x : LocalizedModule S M
⊢ Eq.{u_4 + 1} (α := M'') ((lift S f g h : (a : M') → M'') ((iso S f : (a : LocalizedModule S M) → M') x : M') : M'')
    ((LocalizedModule.lift S g h : (a : LocalizedModule S M) → M'') x : M'')

Tactic:
simp [lift]

Premises used: IsLocalizedModule.lift
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst_7 : IsLocalizedModule S f
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
⊢ lift S f g h ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') = LocalizedModule.lift S g h

Tactic:
LinearMap.ext fun x ↦ lift_iso S f g h x

Premises used: LinearMap.ext, IsLocalizedModule.lift_iso
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
x : M
⊢ Eq.{u_4 + 1} (α := M'') ((lift S f g h : (a : M') → M'') ((f : (a : M) → M') x : M') : M'')
    ((g : (a : M) → M'') x : M'')

Tactic:
LinearMap.congr_fun (lift_comp S f g h) x

Premises used: LocalizedModule.liftOn, IsLocalizedModule.lift_comp, LinearMap.congr_fun, LocalizedModule.lift'
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
rw : (l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M')) ∘ₗ LocalizedModule.mkLinearMap S M = g
⊢ LocalizedModule.lift S g h ∘ₗ (↑(iso S f).symm : M' →ₗ[R] LocalizedModule S M) = l

Tactic:
rw [LocalizedModule.lift_unique S g h (l.comp (iso S f).toLinearMap), LinearMap.comp_assoc,
    LinearEquiv.comp_coe, LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap,
    LinearMap.comp_id]

Premises used: IsLocalizedModule.iso, LocalizedModule.lift_unique, LinearMap.comp_assoc, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_trans_self, LinearEquiv.comp_coe, LinearMap.comp, LinearEquiv.toLinearMap, LinearMap.comp_id
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
rw : l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f
⊢ (l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M')) ∘ₗ LocalizedModule.mkLinearMap S M = g

Tactic:
rw [LinearMap.comp_assoc, ← hl]

Premises used: LinearMap.comp_assoc
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
h₁ :
  ∀ (x : M),
    Eq.{u_4 + 1} (α := M'')
      ((l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M'') x : M'')
      ((l ∘ₗ f : (a : M) → M'') x : M'')
⊢ l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f

Tactic:
ext x
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
x : M
⊢ Eq.{u_4 + 1} (α := M'')
    ((l ∘ₗ (↑(iso S f) : LocalizedModule S M →ₗ[R] M') ∘ₗ LocalizedModule.mkLinearMap S M : (a : M) → M'') x : M'')
    ((l ∘ₗ f : (a : M) → M'') x : M'')

Tactic:
simp
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
⊢ ∀ (g : M →ₗ[R] M''),
    (∀ (x : ↥S),
        IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')) →
      ∃! l : M' →ₗ[R] M'', l ∘ₗ f = g

Tactic:
fun g h => ⟨lift S f g h, lift_comp S f g h, fun l hl => (lift_unique S f g h l hl).symm⟩

Premises used: IsLocalizedModule.lift, IsLocalizedModule.lift_comp, ExistsUnique, And.intro, Exists.intro, IsLocalizedModule.lift_unique, Eq.symm
-- 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
N : Type u_6
N' : Type u_7
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : AddCommMonoid N'
inst_9 : Module R N'
f' : N →ₗ[R] N'
inst_10 : IsLocalizedModule S f'
g g' : M' →ₗ[R] N'
h : g ∘ₗ f = g' ∘ₗ f
⊢ g = g'

Tactic:
(is_universal S f _ <| map_units f').unique h rfl

Premises used: IsLocalizedModule.is_universal, ExistsUnique.unique, IsLocalizedModule.map_units, rfl
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
map_unit :
  ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
hl : k ∘ₗ f = k ∘ₗ f
⊢ j = k

Tactic:
rw [← lift_unique S f (k.comp f) map_unit j h, lift_unique]

Premises used: LinearMap.comp, IsLocalizedModule.lift_unique
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
inst_7 : IsLocalizedModule S f
map_unit :
  ∀ (x : ↥S), IsUnit.{u_4} (M := End R M'') ((algebraMap R (End R M'') : (a : R) → End R M'') (↑x : R) : End R M'')
j k : M' →ₗ[R] M''
h : j ∘ₗ f = k ∘ₗ f
⊢ k ∘ₗ f = k ∘ₗ f

Tactic:
rfl
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst_7 : IsLocalizedModule S f
inst_8 : IsLocalizedModule S g
x : M
⊢ Eq.{u_4 + 1} (α := M'') ((linearEquiv S f g : (a : M') → M'') ((f : (a : M) → M') x : M') : M'')
    ((g : (a : M) → M'') x : M'')

Tactic:
simp [linearEquiv]

Premises used: IsLocalizedModule.linearEquiv
-- 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
M'' : Type u_4
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M''
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst_7 : IsLocalizedModule S f
inst_8 : IsLocalizedModule S g
x : M
⊢ Eq.{u_3 + 1} (α := M') (((linearEquiv S f g).symm : (a : M'') → M') ((g : (a : M) → M'') x : M'') : M')
    ((f : (a : M) → M') x : M')

Tactic:
simp [linearEquiv]

Premises used: IsLocalizedModule.linearEquiv
-- 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
⊢ Function.Injective (β := M') fun (m : M') ↦ s • m

Tactic:
((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units f s)).injective

Premises used: Module.End.isUnit_iff, Function.Bijective.injective, Iff.mp, IsLocalizedModule.map_units
-- 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
m₁ m₂ : M'
⊢ s • m₁ = s • m₂ ↔ m₁ = m₂

Tactic:
(smul_injective f s).eq_iff

Premises used: Function.Injective.eq_iff, 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'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
m : M'
inj : Function.Injective.{u_1 + 1, u_3 + 1} (β := M') fun (r : R) ↦ r • m
s : ↥S
r r' : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ (↑s : R) * x) r) ((fun (x : R) ↦ (↑s : R) * x) r')
⊢ Eq.{u_3 + 1} (α := M') ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r))
    ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r'))

Tactic:
have := congr_arg (· • m) eq
-- 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'
inj : Function.Injective.{u_1 + 1, u_3 + 1} (β := M') fun (r : R) ↦ r • m
s : ↥S
r r' : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ (↑s : R) * x) r) ((fun (x : R) ↦ (↑s : R) * x) r')
this :
  Eq.{u_3 + 1} (α := M') ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r))
    ((fun (x : R) ↦ x • m) ((fun (x : R) ↦ (↑s : R) * x) r'))
⊢ r • m = r' • m

Tactic:
simp_rw [mul_smul, ← Submonoid.smul_def, smul_inj f] at this

Premises used: Submonoid.smul_def, IsLocalizedModule.smul_inj, SemigroupAction.mul_smul
-- 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'
inj : Function.Injective.{u_1 + 1, u_3 + 1} (β := M') fun (r : R) ↦ r • m
s : ↥S
r r' : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ (↑s : R) * x) r) ((fun (x : R) ↦ (↑s : R) * x) r')
this : r • m = r' • m
⊢ r = r'

Tactic:
inj this
-- 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'
inj : Function.Injective.{u_1 + 1, u_3 + 1} (β := M') fun (r : R) ↦ r • m
s : ↥S
r r' : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ (↑s : R) * x) r) ((fun (x : R) ↦ (↑s : R) * x) r')
this : r • m = r' • m
⊢ r = r'

Tactic:
exact inj this
-- 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
r : R
m : M
s : ↥S
delta :
  (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (r • m) s) =
    HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
⊢ mk' f (r • m) s = r • 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
r : R
m : M
s : ↥S
rw :
  (fromLocalizedModule S f : (a : LocalizedModule S M) → M')
      (HSMul.hSMul (β := LocalizedModule S M) r (LocalizedModule.mk m s)) =
    HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
rw₁ rw₂ :
  HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M') =
    HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')
⊢ (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (r • m) s) =
    HSMul.hSMul (β := M') r ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk m s) : M')

Tactic:
rw [← LocalizedModule.smul'_mk, map_smul]

Premises used: LocalizedModule.smul'_mk, map_smul
-- 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 :
  HAdd.hAdd (α := M') (β := 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') =
    (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))
⊢ mk' f m₁ s₁ + mk' f m₂ s₂ = mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * 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₂ : M
s₁ s₂ : ↥S
rw :
  Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M')
        (HAdd.hAdd (α := LocalizedModule S M) (LocalizedModule.mk m₁ s₁) (LocalizedModule.mk m₂ s₂)) :
      M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)) : M')
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)) : M')
    ((fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)) : M')
⊢ HAdd.hAdd (α := M') (β := 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') =
    (fromLocalizedModule S f : (a : LocalizedModule S M) → M') (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))

Tactic:
rw [← map_add, LocalizedModule.mk_add_mk]

Premises used: LocalizedModule.mk_add_mk, map_add