awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.FinitePresentation (goal)
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)
⊢ 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)
have 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)))
    ⊤
Tactic: rw [← LinearMap.range_eq_top] at fsurj ⊢
Cleared hypotheses: fsurj, g
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (hypothesis)
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
⊢ Injective Rₛ Mₛ
have MB : Baer R M
Tactic: have MB : Baer R M := Baer.of_injective ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
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
⊢ Injective Rₛ Mₛ
have 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ₛ)
Tactic: simp only [← Baer.iff_injective, Module.Baer.iff_surjective] at MB ⊢
Cleared hypotheses: MB
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
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ₛ
⊢ ∃ (a : Rₛ →ₗ[Rₛ] Mₛ), (LinearMap.lcomp Rₛ Mₛ (Submodule.subtype Iₛ) : (a : Rₛ →ₗ[Rₛ] Mₛ) → ↥Iₛ →ₗ[Rₛ] Mₛ) a = g
have 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
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]⟩
Cleared hypotheses: Iₛ, g
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (hypothesis)
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ₛ
⊢ ∃ (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
have this : FinitePresentation R ↥I
Tactic: have : FinitePresentation R I := finitePresentation_of_finite R I
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
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 : 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
have 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
Tactic: obtain ⟨⟨g', a⟩, e : a.1 • g = _⟩ := surj S (mapExtendScalars S (I.toLocalized' _ _ _) f Rₛ) g
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨g', rfl⟩ := MB I g'
Cleared hypotheses: g', e
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
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
have 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
Tactic: refine ⟨IsLocalization.mk' Rₛ 1 a • mapExtendScalars S (Algebra.linearMap _ _) f _ g', ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
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)
⊢ Injective R M
have H₁ : ∀ (I : Ideal R) (x : I.IsMaximal), Injective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
Tactic: apply Module.injective_of_localization_maximal
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Injective (goal)
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)
have 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)
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' := ?_ }
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
X : ModuleCat.{v, u} R
inj : Injective X
h : Small.{v, u} (Localization (M := R) S) := ⋯
⊢ Injective ((localizedModuleFunctor S).obj X)
have rw : ∀ (inj : Module.Injective.{u, v} R (↑X : Type v)),
  Module.Injective.{u, v} (Localization (M := R) S) (↑((localizedModuleFunctor.{v, u} S).1 X) : Type v)
Tactic: rw [← Module.injective_iff_injective_object] at inj ⊢
Cleared hypotheses: inj, h
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
S : Submonoid R
M : ModuleCat.{v, u} R
inst_3 : HasInjectiveDimensionLE M n
⊢ HasInjectiveDimensionLE (M.localizedModule S) n
have this : Small.{v, u} (Localization (M := R) S)
Tactic: have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_3 injle : HasInjectiveDimensionLE M 0
⊢ HasInjectiveDimensionLE (M.localizedModule S) 0
have zero : ∀ (injle : Injective M), Injective (M.localizedModule S)
Tactic: simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]
      at injle ⊢
Cleared hypotheses: injle
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
M : ModuleCat.{v, u} R
inst_3 : HasInjectiveDimensionLE M 0
injle : Injective M
⊢ Injective (M.localizedModule S)
have zero : ∀ (injle : Module.Injective.{u, v} R (↑M : Type v)),
  Module.Injective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)
Tactic: rw [← Module.injective_iff_injective_object] at injle ⊢
Cleared hypotheses: injle
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_3 : HasInjectiveDimensionLE M (n + 1)
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
have ei : EnoughInjectives (ModuleCat.{v, u} R)
Tactic: have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_3 : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat.{v, u} R)
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
have succ : ∀ (I : ModuleCat.{v, u} R) (inj : Injective I) (f : M ⟶ I) (monof : Mono f),
  HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
Tactic: rcases ei.1 M with ⟨I, inj, f, monof⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_3 : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat.{v, u} R)
I : ModuleCat.{v, u} R
inj : Injective I
f : M ⟶ I
monof : Mono f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
have T_exact : T.ShortExact
Tactic: have T_exact : T.ShortExact := { exact := ShortComplex.exact_cokernel f }
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization (M := R) S)
n : ℕ
ih : ∀ (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n
M : ModuleCat.{v, u} R
inst_3 : HasInjectiveDimensionLE M (n + 1)
ei : EnoughInjectives (ModuleCat.{v, u} R)
I : ModuleCat.{v, u} R
inj : Injective I
f : M ⟶ I
monof : Mono f
T : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
T_exact : T.ShortExact
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
have T_exact' : Function.Exact (M := (↑T.X₁ : Type v)) (N := (↑T.X₂ : Type v)) (P := (↑T.X₃ : Type v))
  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
        T.f) :
    (a : (↑T.X₁ : Type v)) → (↑T.X₂ : Type v))
  (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier)
        T.g) :
    (a : (↑T.X₂ : Type v)) → (↑T.X₃ : Type v))
Tactic: have T_exact' : Function.Exact (ConcreteCategory.hom T.f) (ConcreteCategory.hom T.g) :=
      (ShortComplex.ShortExact.moduleCat_exact_iff_function_exact _).mp T_exact.1