awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
this :
  Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
h : M' →ₗ[R] N'
h₁ :
  (((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
        (a : M' →ₗ[R] N') → M' →ₗ[R] N')
      ((↑⋯.unit⁻¹ : End R N') ∘ₗ h) =
    h
⊢ ∃ (a : M' →ₗ[R] N'),
    (((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
          (a : M' →ₗ[R] N') → M' →ₗ[R] N')
        a =
      h

Tactic:
use ((IsLocalizedModule.map_units (S := S) (f := g) s).unit⁻¹).1 ∘ₗ h

Premises used: Units.val, Inv.inv, IsUnit.unit, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
this :
  Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
h : M' →ₗ[R] N'
h₁ :
  ∀ (x : M'),
    Eq.{u_2 + 1} (α := N')
      ((((((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
                  (a : M' →ₗ[R] N') → M' →ₗ[R] N')
                ((↑⋯.unit⁻¹ : End R N') ∘ₗ h) :
              M' →ₗ[R] N') :
            (a : M') → N')
          x :
        N')
      ((h : (a : M') → N') x : N')
⊢ (((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
        (a : M' →ₗ[R] N') → M' →ₗ[R] N')
      ((↑⋯.unit⁻¹ : End R N') ∘ₗ h) =
    h

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
this :
  Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
h : M' →ₗ[R] N'
x : M'
⊢ Eq.{u_2 + 1} (α := N')
    ((((((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
                (a : M' →ₗ[R] N') → M' →ₗ[R] N')
              ((↑⋯.unit⁻¹ : End R N') ∘ₗ h) :
            M' →ₗ[R] N') :
          (a : M') → N')
        x :
      N')
    ((h : (a : M') → N') x : N')

Tactic:
Module.End.isUnit_apply_inv_apply_of_isUnit
        (IsLocalizedModule.map_units (S := S) (f := g) s) (h x)

Premises used: IsLocalizedModule.map_units, Module.End.isUnit_apply_inv_apply_of_isUnit, DFunLike.coe
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
s : ↥S
this :
  Function.Bijective.{u_2 + 1, u_2 + 1} (α := N') (β := N')
    (⇑((algebraMap R (End R N') : (a : R) → End R N') (↑s : R) : End R N') : (a : N') → N')
h : M' →ₗ[R] N'
x : M'
⊢ Eq.{u_2 + 1} (α := N')
    ((((((algebraMap R (End R (M' →ₗ[R] N')) : (a : R) → End R (M' →ₗ[R] N')) (↑s : R) : End R (M' →ₗ[R] N')) :
                (a : M' →ₗ[R] N') → M' →ₗ[R] N')
              ((↑⋯.unit⁻¹ : End R N') ∘ₗ h) :
            M' →ₗ[R] N') :
          (a : M') → N')
        x :
      N')
    ((h : (a : M') → N') x : N')

Tactic:
exact Module.End.isUnit_apply_inv_apply_of_isUnit
        (IsLocalizedModule.map_units (S := S) (f := g) s) (h x)

Premises used: IsLocalizedModule.map_units, Module.End.isUnit_apply_inv_apply_of_isUnit, DFunLike.coe
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h : M' →ₗ[R] N'
surj :
  ∀ (h' : M →ₗ[R] N) (s : ↥S) (e : g ∘ₗ h' = s • h ∘ₗ f),
    ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1
⊢ ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1

Tactic:
obtain ⟨h', s, e⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (h ∘ₗ f)

Premises used: Module.FinitePresentation.exists_lift_of_isLocalizedModule, LinearMap.comp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1

Tactic:
⟨⟨h', s⟩, ?_⟩

Premises used: Prod.mk, Exists.intro
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
surj : (h', s).2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1
⊢ ∃ (x : (M →ₗ[R] N) × ↥S), x.2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') x.1

Tactic:
refine ⟨⟨h', s⟩, ?_⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
surj : ((h', s).2 • h) ∘ₗ f = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f
⊢ (h', s).2 • h = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1

Tactic:
apply IsLocalizedModule.ext S f (IsLocalizedModule.map_units g)

Premises used: IsLocalizedModule.ext, IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
h₁ :
  ∀ (x : M),
    Eq.{u_2 + 1} (α := N') ((g ∘ₗ h' : (a : M) → N') x : N')
      (((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f : (a : M) → N') x : N')
⊢ g ∘ₗ h' = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
x : M
⊢ Eq.{u_2 + 1} (α := N') ((g ∘ₗ h' : (a : M) → N') x : N')
    (((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f : (a : M) → N') x : N')

Tactic:
simp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h : M' →ₗ[R] N'
h' : M →ₗ[R] N
s : ↥S
e : g ∘ₗ h' = s • h ∘ₗ f
⊢ ((h', s).2 • h) ∘ₗ f = (IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') (h', s).1 ∘ₗ f

Tactic:
refine e.symm.trans (by ext; simp)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h₁ h₂ : M →ₗ[R] N
e :
  Eq (α := M' →ₗ[R] N') ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₁ : M' →ₗ[R] N')
    ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₂ : M' →ₗ[R] N')
exists_of_eq : g ∘ₗ h₁ = g ∘ₗ h₂
⊢ ∃ (c : ↥S), c • h₁ = c • h₂

Tactic:
apply Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g

Premises used: Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h₁ h₂ : M →ₗ[R] N
e :
  Eq (α := M' →ₗ[R] N') ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₁ : M' →ₗ[R] N')
    ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₂ : M' →ₗ[R] N')
exists_of_eq : ∀ (x : M), Eq.{u_2 + 1} (α := N') ((g ∘ₗ h₁ : (a : M) → N') x : N') ((g ∘ₗ h₂ : (a : M) → N') x : N')
⊢ g ∘ₗ h₁ = g ∘ₗ h₂

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.606025
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : FinitePresentation R M
h₁ h₂ : M →ₗ[R] N
e :
  Eq (α := M' →ₗ[R] N') ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₁ : M' →ₗ[R] N')
    ((IsLocalizedModule.map S f g : (a : M →ₗ[R] N) → M' →ₗ[R] N') h₂ : M' →ₗ[R] N')
x : M
⊢ Eq.{u_2 + 1} (α := N') ((g ∘ₗ h₁ : (a : M) → N') x : N') ((g ∘ₗ h₂ : (a : M) → N') x : N')

Tactic:
simpa using LinearMap.congr_fun e (f x)

Premises used: LinearMap.congr_fun, DFunLike.coe
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_4
M : Type u_5
N : Type u_6
N'_1 : Type ?u.626285
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
Rₛ : Type u_3
inst_14 : CommRing Rₛ
inst_15 : Algebra R Rₛ
inst_16 : Module Rₛ M'
inst_17 : Module Rₛ N'
inst_18 : IsScalarTower R Rₛ M'
inst_19 : IsScalarTower R Rₛ N'
inst_20 : IsLocalization S Rₛ
inst_21 : FinitePresentation R M
⊢ IsLocalizedModule (M' := M' →ₗ[Rₛ] N') S
    (IsLocalizedModule.mapExtendScalars S f g Rₛ : (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N')

Tactic:
IsLocalizedModule.of_linearEquiv _ _ _

Premises used: IsLocalizedModule.of_linearEquiv, IsLocalizedModule.mapExtendScalars
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
N'_1 : Type ?u.638711
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'_1
inst_6 : Module R N'_1
S : Submonoid R
f_1 : N →ₗ[R] N'_1
inst_7 : IsLocalizedModule S f_1
M' : Type u_1
inst_8 : AddCommGroup M'
inst_9 : Module R M'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
N' : Type u_2
inst_11 : AddCommGroup N'
inst_12 : Module R N'
g : N →ₗ[R] N'
inst_13 : IsLocalizedModule S g
inst_14 : Module.FinitePresentation R M
⊢ IsLocalizedModule (M := M →ₗ[R] N) S (LocalizedModule.map S)

Tactic:
Module.FinitePresentation.isLocalizedModule_mapExtendScalars _ _ _ _

Premises used: LocalizedModule.map, Module.FinitePresentation.isLocalizedModule_mapExtendScalars
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
y : M'
⊢ HSMul.hSMul.{u_3, u_1, u_1} (α := ↥S) (y, 1).2 y = (LinearMap.id : (a : M') → M') (y, 1).1

Tactic:
simp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
⊢ ∀ {x₁ x₂ : M'},
    Eq (α := M') ((LinearMap.id : (a : M') → M') x₁ : M') ((LinearMap.id : (a : M') → M') x₂ : M') →
      ∃ (c : ↥S), c • x₁ = c • x₂

Tactic:
simpa using ⟨1, S.one_mem⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
⊢ IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id

Tactic:
have : IsLocalizedModule S (.id (R := R) (M := M')) :=
    ⟨IsLocalizedModule.map_units f, fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, S.one_mem⟩⟩
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := M') (β := M') (⇑LinearMap.id : (a : M') → M')

Tactic:
show Function.Bijective LinearMap.id from Function.bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
h :
  Eq.{u_1 + 1} (α := M' →ₗ[R] M') ((map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f : M' →ₗ[R] M')
    (LinearMap.id : M' →ₗ[R] M')
⊢ Function.Bijective.{u_1 + 1, u_1 + 1} (α := M') (β := M')
    (⇑((map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f : M' →ₗ[R] M') : (a : M') → M')

Tactic:
convert! show Function.Bijective LinearMap.id from Function.bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
h :
  ∀ (x : ↥S),
    IsUnit.{u_1} (M := Module.End R M')
      ((algebraMap R (Module.End R M') : (a : R) → Module.End R M') (↑x : R) : Module.End R M')
h₁ : (map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f ∘ₗ f = LinearMap.id ∘ₗ f
⊢ Eq.{u_1 + 1} (α := M' →ₗ[R] M') ((map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f : M' →ₗ[R] M')
    (LinearMap.id : M' →ₗ[R] M')

Tactic:
apply IsLocalizedModule.ext S f

Premises used: IsLocalizedModule.ext
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
⊢ ∀ (x : ↥S),
    IsUnit.{u_1} (M := Module.End R M')
      ((algebraMap R (Module.End R M') : (a : R) → Module.End R M') (↑x : R) : Module.End R M')

Tactic:
IsLocalizedModule.map_units f

Premises used: IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
⊢ ∀ (x : ↥S),
    IsUnit.{u_1} (M := Module.End R M')
      ((algebraMap R (Module.End R M') : (a : R) → Module.End R M') (↑x : R) : Module.End R M')

Tactic:
exact IsLocalizedModule.map_units f

Premises used: IsLocalizedModule.map_units
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
⊢ (map S f LinearMap.id : (a : M →ₗ[R] M') → M' →ₗ[R] M') f ∘ₗ f = LinearMap.id ∘ₗ f

Tactic:
simp [IsLocalizedModule.map_comp]

Premises used: IsLocalizedModule.map_comp
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
obtain :
  ∀ (r : R) (hrp : r ∈ S)
    (H :
      ∀ (t : R),
        r ∣ t →
          Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β :=
            LocalizedModule (Submonoid.powers t) M')
            (⇑((LocalizedModule.map (Submonoid.powers t) :
                      (a : M →ₗ[R] M') →
                        LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                          LocalizedModule (Submonoid.powers t) M')
                    f :
                  LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                    (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
              (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')),
    ∃ r ∈ S, IsLocalizedModule.Away r f
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f

Tactic:
obtain ⟨r, hrp, H⟩ := exists_bijective_map_powers S
      f (.id (R := R) (M := M')) f <| by
    convert! show Function.Bijective LinearMap.id from Function.bijective_id
    apply IsLocalizedModule.ext S f
    · exact IsLocalizedModule.map_units f
    · simp [IsLocalizedModule.map_comp]

Premises used: LinearMap.id, exists_bijective_map_powers