awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
g : (↑s : Type u_1)
hl :
  ∀ (fsurj : f.range = ⊤) (g : (↑s : Type u_1)),
    Eq.{u_3 + 1} (α := Submodule.{u_4, u_3} (Rₚ g) (Mₚ g))
      (LinearMap.range (M := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R))
        (LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (↑g : R)) (Rₚ g)
          ((IsLocalizedModule.map (Submonoid.powers (↑g : R))
                ((fun (g : (↑s : Type u_1)) ↦
                    ((TensorProduct.mk R (Rₚ g) (Fin n → R) :
                          (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
                        1 :
                      (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
                  g)
                (ϕ g) :
              (a : (Fin n → R) →ₗ[R] M) → TensorProduct R (Rₚ g) (Fin n → R) →ₗ[R] Mₚ g)
            f)))
      ⊤
⊢ Function.Surjective (α := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)) (β := Mₚ g)
    (⇑(LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (↑g : R)) (Rₚ g)
            ((IsLocalizedModule.map (Submonoid.powers (↑g : R))
                  ((fun (g : (↑s : Type u_1)) ↦
                      ((TensorProduct.mk R (Rₚ g) (Fin n → R) :
                            (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
                          1 :
                        (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
                    g)
                  (ϕ g) :
                (a : (Fin n → R) →ₗ[R] M) → TensorProduct R (Rₚ g) (Fin n → R) →ₗ[R] Mₚ g)
              f) :
          LinearMap (R := Rₚ g) (RingHom.id (Rₚ g)) (TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)) (Mₚ g)) :
      (a : TensorProduct R (Rₚ g) (Fin n → R)) → Mₚ g)

Tactic:
rw [← LinearMap.range_eq_top] at fsurj ⊢

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_3
inst_3 : (g : (↑s : Type u_1)) → AddCommGroup (Mₚ g)
inst_4 : (g : (↑s : Type u_1)) → Module.{u_1, u_3} R (Mₚ g)
Rₚ : (↑s : Type u_1) → Type u_4
inst_5 : (g : (↑s : Type u_1)) → CommRing (Rₚ g)
inst_6 : (g : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u_1)) → Module.{u_4, u_3} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_3} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u_1)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
h : ∀ (g : (↑s : Type u_1)), FinitePresentation.{u_4, u_3} (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : f.range = ⊤
g : (↑s : Type u_1)
⊢ Eq.{u_3 + 1} (α := Submodule.{u_4, u_3} (Rₚ g) (Mₚ g))
    (LinearMap.range (M := TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R))
      (LinearMap.extendScalarsOfIsLocalization (Submonoid.powers (↑g : R)) (Rₚ g)
        ((IsLocalizedModule.map (Submonoid.powers (↑g : R))
              ((fun (g : (↑s : Type u_1)) ↦
                  ((TensorProduct.mk R (Rₚ g) (Fin n → R) :
                        (a : Rₚ g) → (Fin n → R) →ₗ[R] TensorProduct R (Rₚ g) (Fin n → R))
                      1 :
                    (Fin n → R) →ₗ[R] TensorProduct.{u_1, u_4, u_1} R (Rₚ g) (Fin n → R)))
                g)
              (ϕ g) :
            (a : (Fin n → R) →ₗ[R] M) → TensorProduct R (Rₚ g) (Fin n → R) →ₗ[R] Mₚ g)
          f)))
    ⊤

Tactic:
simp [← LinearMap.localized'_range_eq_range_localizedMap (Rₚ g) (Submonoid.powers g.1), fsurj]

Premises used: LinearMap.localized'_range_eq_range_localizedMap, Submonoid.powers, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.FinitePresentation
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
h : ∀ (g : (↑s : Type u_1)), FinitePresentation (Localization.Away (↑g : R)) (LocalizedModule.Away (↑g : R) M)
⊢ FinitePresentation R M

Tactic:
of_localizationSpan' s hs (fun g ↦ LocalizedModule.mkLinearMap (Submonoid.powers g.1) M) h

Premises used: Module.FinitePresentation.of_localizationSpan', Submonoid.powers, LocalizedModule.mkLinearMap, Subtype.val
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
⊢ Baer R M

Tactic:
have MB : Baer R M := Baer.of_injective ‹_›
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB : Baer R M
simp :
  ∀
    (MB :
      ∀ (I : Ideal R),
        Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
          (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M))
    (I : Ideal Rₛ),
    Function.Surjective (α := Rₛ →ₗ[Rₛ] Mₛ) (β := ↥I →ₗ[Rₛ] Mₛ)
      (⇑(LinearMap.lcomp Rₛ Mₛ (Submodule.subtype I)) : (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥I →ₗ[Rₛ] Mₛ)
⊢ Injective Rₛ Mₛ

Tactic:
simp only [← Baer.iff_injective, Module.Baer.iff_surjective] at MB ⊢

Premises used: Module.Baer.iff_surjective, Module.Baer.iff_injective
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
Iₛ : Ideal Rₛ
g : ↥Iₛ →ₗ[Rₛ] Mₛ
⊢ Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) (Ideal.comap (F := R →+* Rₛ) (algebraMap R Rₛ) Iₛ) = Iₛ

Tactic:
simp [Ideal.localized'_eq_map, IsLocalization.map_under S]

Premises used: Ideal.localized'_eq_map, IsLocalization.map_under
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
Iₛ : Ideal Rₛ
g : ↥Iₛ →ₗ[Rₛ] Mₛ
obtain :
  ∀ (I : Submodule R R) (g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ),
    ∃ (a : Rₛ →ₗ[Rₛ] Mₛ),
      (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
            (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
          a =
        g
⊢ ∃ (a : Rₛ →ₗ[Rₛ] Mₛ), (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype Iₛ) : (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥Iₛ →ₗ[Rₛ] Mₛ) a = g

Tactic:
obtain ⟨I, rfl⟩ : ∃ I, .localized' Rₛ S (Algebra.linearMap R Rₛ) I = Iₛ :=
    ⟨Iₛ.comap (algebraMap R Rₛ), by simp [Ideal.localized'_eq_map, IsLocalization.map_under S]⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
⊢ FinitePresentation R ↥I

Tactic:
have : FinitePresentation R I := finitePresentation_of_finite R I
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
obtain :
  ∀ (g' : ↥I →ₗ[R] M) (a : ↥S)
    (e :
      (↑a : R) • g =
        ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
              (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
            (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
          (g', a).1),
    ∃ (a : Rₛ →ₗ[Rₛ] Mₛ),
      (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
            (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
          a =
        g
⊢ ∃ (a : Rₛ →ₗ[Rₛ] Mₛ),
    (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
          (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        a =
      g

Tactic:
obtain ⟨⟨g', a⟩, e : a.1 • g = _⟩ := surj S (mapExtendScalars S (I.toLocalized' _ _ _) f Rₛ) g

Premises used: Submodule.toLocalized', IsLocalizedModule.mapExtendScalars, IsLocalizedModule.surj
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
g' : ↥I →ₗ[R] M
a : ↥S
e :
  (↑a : R) • g =
    ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
          (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
        (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
      (g', a).1
obtain :
  ∀ (g' : R →ₗ[R] M)
    (e :
      (↑a : R) • g =
        ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
              (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
            (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
          ((LinearMap.lcomp R M I.subtype : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g', a).1),
    ∃ (a : Rₛ →ₗ[Rₛ] Mₛ),
      (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
            (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
          a =
        g
⊢ ∃ (a : Rₛ →ₗ[Rₛ] Mₛ),
    (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
          (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        a =
      g

Tactic:
obtain ⟨g', rfl⟩ := MB I g'

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  (↑a : R) • g =
    ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
          (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
        (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
      ((LinearMap.lcomp R M I.subtype : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g', a).1
⊢ ∃ (a : Rₛ →ₗ[Rₛ] Mₛ),
    (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
          (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        a =
      g

Tactic:
⟨IsLocalization.mk' Rₛ 1 a • mapExtendScalars S (Algebra.linearMap _ _) f _ g', ?_⟩

Premises used: Algebra.linearMap, IsLocalization.mk', Exists.intro, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, IsLocalizedModule.mapExtendScalars
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
inst_3 : Small.{v, u} R
inst_4 : IsNoetherianRing R
Rₛ : Type u'
inst_5 : Small.{v', u'} Rₛ
inst_6 : CommRing Rₛ
inst_7 : Algebra R Rₛ
Mₛ : Type v'
inst_8 : AddCommGroup Mₛ
inst_9 : Module R Mₛ
inst_10 : Module Rₛ Mₛ
inst_11 : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst_12 : IsLocalization S Rₛ
inst_13 : IsLocalizedModule S f
inst_14 : Injective R M
MB :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Submodule R R
g : ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ
this : FinitePresentation R ↥I
a : ↥S
g' : R →ₗ[R] M
e :
  (↑a : R) • g =
    ((mapExtendScalars S (Submodule.toLocalized' Rₛ S (Algebra.linearMap R Rₛ) I) f Rₛ :
          (↥I →ₗ[R] M) →ₗ[R] ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ) :
        (a : ↥I →ₗ[R] M) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
      ((LinearMap.lcomp R M I.subtype : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g', a).1
refine :
  (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
        (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
      (HSMul.hSMul (β := Rₛ →ₗ[Rₛ] Mₛ) (IsLocalization.mk' Rₛ 1 a)
        (((mapExtendScalars S (Algebra.linearMap R Rₛ) f Rₛ : (R →ₗ[R] M) →ₗ[R] Rₛ →ₗ[Rₛ] Mₛ) :
              (a : R →ₗ[R] M) → Rₛ →ₗ[Rₛ] Mₛ)
            g' :
          Rₛ →ₗ[Rₛ] Mₛ)) =
    g
⊢ ∃ (a : Rₛ →ₗ[Rₛ] Mₛ),
    (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype (Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I)) :
          (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥(Submodule.localized' Rₛ S (Algebra.linearMap R Rₛ) I) →ₗ[Rₛ] Mₛ)
        a =
      g

Tactic:
refine ⟨IsLocalization.mk' Rₛ 1 a • mapExtendScalars S (Algebra.linearMap _ _) f _ g', ?_⟩
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst_1 : CommRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u, u'} R (Rₚ P)
inst_7 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u, u'} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u, v'} R (Mₚ P)
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u', v'} (Rₚ P) (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u, u', v'} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u, u, v, v'} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
inst_12 : Small.{v, u} R
inst_13 : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective.{u', v'} (Rₚ I) (Mₚ I)
H₁ : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
⊢ Injective R M

Tactic:
apply Module.injective_of_localization_maximal

Premises used: Module.injective_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst_1 : CommRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u, u'} R (Rₚ P)
inst_7 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u, u'} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u, v'} R (Mₚ P)
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u', v'} (Rₚ P) (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u, u', v'} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u, u, v, v'} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
inst_12 : Small.{v, u} R
inst_13 : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective.{u', v'} (Rₚ I) (Mₚ I)
P : Ideal R
hP : P.IsMaximal
⊢ Injective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)

Tactic:
Module.Injective.of_ringEquiv (M := Mₚ P)
    (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
    { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P)
        (LocalizedModule.mkLinearMap P.primeCompl M)
      map_smul' := ?_ }

Premises used: LinearEquiv.right_inv, LinearEquiv.mk, IsLocalizedModule.linearEquiv, Localization.AtPrime, LinearEquiv.left_inv, LinearMap.toAddHom, Module.Injective.of_ringEquiv, LinearEquiv.invFun, LinearEquiv.toLinearMap, IsLocalization.algEquiv, AlgEquiv.toRingEquiv, LinearMap.mk, LocalizedModule.mkLinearMap, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.Injective
Goal:
R : Type u
inst_1 : CommRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u'
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst : P.IsMaximal], Small.{v', u'} (Rₚ P)
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → Algebra.{u, u'} R (Rₚ P)
inst_7 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime.{u, u'} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type v'
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u, v'} R (Mₚ P)
inst_10 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u', v'} (Rₚ P) (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower.{u, u', v'} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → LinearMap.{u, u, v, v'} (RingHom.id R) M (Mₚ P)
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
inst_12 : Small.{v, u} R
inst_13 : IsNoetherianRing R
H : ∀ (I : Ideal R) (x : I.IsMaximal), Injective.{u', v'} (Rₚ I) (Mₚ I)
P : Ideal R
hP : P.IsMaximal
H₁ :
  ∀ (m : Rₚ P) (x : Mₚ P),
    AddHom.toFun
        (LinearMap.toAddHom
          (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
            Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
        (m • x) =
      HSMul.hSMul (α := Localization.AtPrime P)
        ((((↑(AlgEquiv.toRingEquiv (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)) :
                      RingEquiv.{u', u} (Rₚ P) (Localization.AtPrime P)) :
                  RingHom.{u', u} (Rₚ P) (Localization.AtPrime P)) :
                RingHom.{u', u} (Rₚ P) (Localization.AtPrime P)) :
              (a : Rₚ P) → Localization.AtPrime P)
            m :
          Localization.AtPrime P)
        (AddHom.toFun
          (LinearMap.toAddHom
            (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M)) :
              Mₚ P →ₗ[R] LocalizedModule P.primeCompl M))
          x)
⊢ Injective (Localization.AtPrime P) (LocalizedModule P.primeCompl M)

Tactic:
refine Module.Injective.of_ringEquiv (M := Mₚ P)
    (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
    { __ := IsLocalizedModule.linearEquiv P.primeCompl (f P)
        (LocalizedModule.mkLinearMap P.primeCompl M)
      map_smul' := ?_ }

Premises used: LinearEquiv.right_inv, LinearEquiv.mk, IsLocalizedModule.linearEquiv, Localization.AtPrime, LinearEquiv.left_inv, LinearMap.toAddHom, Module.Injective.of_ringEquiv, LinearEquiv.invFun, LinearEquiv.toLinearMap, IsLocalization.algEquiv, AlgEquiv.toRingEquiv, LinearMap.mk, LocalizedModule.mkLinearMap, Ideal.primeCompl