awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : Mₚ P
r : R
s : ↥P.primeCompl
⊢ HSMul.hSMul (β := LocalizedModule P.primeCompl M) (↑s : R)
      ((IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M) :
            (a : Mₚ P) → LocalizedModule P.primeCompl M)
          (HSMul.hSMul.{u', v', v'} (α := Rₚ P) (IsLocalization.mk' (Rₚ P) r s) m) :
        LocalizedModule P.primeCompl M) =
    (↑s : R) •
      HSMul.hSMul (α := Localization.AtPrime P) (β := LocalizedModule P.primeCompl M)
        ((IsLocalization.map (M := P.primeCompl) (T := P.primeCompl) (Localization.AtPrime P) (RingHom.id R) ⋯ :
            (a : Rₚ P) → Localization.AtPrime P)
          (IsLocalization.mk' (Rₚ P) r s))
        ((IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M) :
              (a : Mₚ P) → LocalizedModule P.primeCompl M)
            m :
          LocalizedModule P.primeCompl M)

Tactic:
simp only [← map_smul, ← smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul,
      IsLocalization.map_id_mk']

Premises used: smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul, IsLocalization.map_id_mk', map_smul
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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) := ⋯
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)
⊢ Injective ((localizedModuleFunctor S).obj X)

Tactic:
rw [← Module.injective_iff_injective_object] at inj ⊢

Premises used: Module.injective_iff_injective_object
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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 : Module.Injective.{u, v} R (↑X : Type v)
h : Small.{v, u} (Localization (M := R) S) := ⋯
⊢ Module.Injective.{u, v} (Localization (M := R) S) (↑((localizedModuleFunctor.{v, u} S).1 X) : Type v)

Tactic:
simpa [ModuleCat.localizedModuleFunctor] using
      Module.injective_of_isLocalizedModule S (X.localizedModuleMkLinearMap S)

Premises used: ModuleCat.localizedModuleFunctor, ModuleCat.localizedModuleMkLinearMap, Module.injective_of_isLocalizedModule
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
⊢ Small.{v, u} (Localization (M := R) S)

Tactic:
have : Small.{v} (Localization S) := small_of_surjective Localization.mkHom_surjective
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
⊢ HasInjectiveDimensionLE M 0

Tactic:
have injle : HasInjectiveDimensionLE M 0 := ‹_›
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
zero : ∀ (injle : Injective M), Injective (M.localizedModule S)
⊢ HasInjectiveDimensionLE (M.localizedModule S) 0

Tactic:
simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]
      at injle ⊢

Premises used: CategoryTheory.HasInjectiveDimensionLE, zero_add, CategoryTheory.injective_iff_hasInjectiveDimensionLT_one
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
zero :
  ∀ (injle : Module.Injective.{u, v} R (↑M : Type v)),
    Module.Injective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)
⊢ Injective (M.localizedModule S)

Tactic:
rw [← Module.injective_iff_injective_object] at injle ⊢

Premises used: Module.injective_iff_injective_object
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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 : Module.Injective.{u, v} R (↑M : Type v)
⊢ Module.Injective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)

Tactic:
Module.injective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)

Premises used: ModuleCat.localizedModuleMkLinearMap, Module.injective_of_isLocalizedModule
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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 : Module.Injective.{u, v} R (↑M : Type v)
⊢ Module.Injective.{u, v} (Localization (M := R) S) (↑(M.localizedModule S) : Type v)

Tactic:
exact Module.injective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)

Premises used: ModuleCat.localizedModuleMkLinearMap, Module.injective_of_isLocalizedModule
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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)
⊢ EnoughInjectives (ModuleCat.{v, u} R)

Tactic:
have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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)
succ :
  ∀ (I : ModuleCat.{v, u} R) (inj : Injective I) (f : M ⟶ I) (monof : Mono f),
    HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
rcases ei.1 M with ⟨I, inj, f, monof⟩

Premises used: CategoryTheory.EnoughInjectives.presentation
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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.ShortExact

Tactic:
have T_exact : T.ShortExact := { exact := ShortComplex.exact_cokernel f }
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
⊢ 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
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
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))
⊢ Function.Exact (M := (↑(T.X₁.localizedModule S) : Type v)) (N := (↑(T.X₂.localizedModule S) : Type v)) (P :=
    (↑(T.X₃.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₁.localizedModuleMkLinearMap S) (T.X₂.localizedModuleMkLinearMap S) :
              (a : (↑T.X₁ : Type v) →ₗ[R] (↑T.X₂ : Type v)) →
                (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.f) :
          (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v)) :
      (a : (↑(T.X₁.localizedModule S) : Type v)) → (↑(T.X₂.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) :
              (a : (↑T.X₂ : Type v) →ₗ[R] (↑T.X₃ : Type v)) →
                (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.g) :
          (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v)) :
      (a : (↑(T.X₂.localizedModule S) : Type v)) → (↑(T.X₃.localizedModule S) : Type v))

Tactic:
have TS_exact' := IsLocalizedModule.map_exact S (T.X₁.localizedModuleMkLinearMap S)
      (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) _ _ T_exact'
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
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))
TS_exact' :
  Function.Exact (M := (↑(T.X₁.localizedModule S) : Type v)) (N := (↑(T.X₂.localizedModule S) : Type v)) (P :=
    (↑(T.X₃.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₁.localizedModuleMkLinearMap S) (T.X₂.localizedModuleMkLinearMap S) :
              (a : (↑T.X₁ : Type v) →ₗ[R] (↑T.X₂ : Type v)) →
                (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.f) :
          (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v)) :
      (a : (↑(T.X₁.localizedModule S) : Type v)) → (↑(T.X₂.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) :
              (a : (↑T.X₂ : Type v) →ₗ[R] (↑T.X₃ : Type v)) →
                (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.g) :
          (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v)) :
      (a : (↑(T.X₂.localizedModule S) : Type v)) → (↑(T.X₃.localizedModule S) : Type v))
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
⊢ TS.ShortExact

Tactic:
have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
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))
TS_exact' :
  Function.Exact (M := (↑(T.X₁.localizedModule S) : Type v)) (N := (↑(T.X₂.localizedModule S) : Type v)) (P :=
    (↑(T.X₃.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₁.localizedModuleMkLinearMap S) (T.X₂.localizedModuleMkLinearMap S) :
              (a : (↑T.X₁ : Type v) →ₗ[R] (↑T.X₂ : Type v)) →
                (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.f) :
          (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v)) :
      (a : (↑(T.X₁.localizedModule S) : Type v)) → (↑(T.X₂.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) :
              (a : (↑T.X₂ : Type v) →ₗ[R] (↑T.X₃ : Type v)) →
                (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.g) :
          (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v)) :
      (a : (↑(T.X₂.localizedModule S) : Type v)) → (↑(T.X₃.localizedModule S) : Type v))
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
h : HasInjectiveDimensionLT T.X₃ (n + 1) := ⋯
h_1 : Injective TS.X₂ := ⋯
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
(TS_exact.hasInjectiveDimensionLT_X₃_iff n ‹_›).mp (ih T.X₃)

Premises used: Iff.mp, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff, ModuleCat.localizedModule, CategoryTheory.ShortComplex.X₃
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
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))
TS_exact' :
  Function.Exact (M := (↑(T.X₁.localizedModule S) : Type v)) (N := (↑(T.X₂.localizedModule S) : Type v)) (P :=
    (↑(T.X₃.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₁.localizedModuleMkLinearMap S) (T.X₂.localizedModuleMkLinearMap S) :
              (a : (↑T.X₁ : Type v) →ₗ[R] (↑T.X₂ : Type v)) →
                (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.f) :
          (↑(T.X₁.localizedModule S) : Type v) →ₗ[R] (↑(T.X₂.localizedModule S) : Type v)) :
      (a : (↑(T.X₁.localizedModule S) : Type v)) → (↑(T.X₂.localizedModule S) : Type v))
    (⇑((IsLocalizedModule.map S (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) :
              (a : (↑T.X₂ : Type v) →ₗ[R] (↑T.X₃ : Type v)) →
                (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v))
            (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC :=
              carrier) T.g) :
          (↑(T.X₂.localizedModule S) : Type v) →ₗ[R] (↑(T.X₃.localizedModule S) : Type v)) :
      (a : (↑(T.X₂.localizedModule S) : Type v)) → (↑(T.X₃.localizedModule S) : Type v))
TS : ShortComplex (ModuleCat.{v, u} (Localization (M := R) S)) := T.map (localizedModuleFunctor S)
TS_exact : TS.ShortExact
h : HasInjectiveDimensionLT T.X₃ (n + 1) := ⋯
h_1 : Injective TS.X₂ := ⋯
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)

Tactic:
exact (TS_exact.hasInjectiveDimensionLT_X₃_iff n ‹_›).mp (ih T.X₃)

Premises used: Iff.mp, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff, CategoryTheory.ShortComplex.X₃
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
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
this : Small.{v, u} (Localization (M := R) S)
zero : ∀ (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M 0], HasInjectiveDimensionLE (M.localizedModule S) 0
succ :
  ∀ (n : ℕ)
    (ih : ∀ (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M n], HasInjectiveDimensionLE (M.localizedModule S) n)
    (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M (n + 1)], HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
⊢ HasInjectiveDimensionLE (M.localizedModule S) n

Tactic:
induction n generalizing M with
  | zero =>
    have injle : HasInjectiveDimensionLE M 0 := ‹_›
    simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]
      at injle ⊢
    rw [← Module.injective_iff_injective_object] at injle ⊢
    exact Module.injective_of_isLocalizedModule S (M.localizedModuleMkLinearMap S)
  | succ n ih =>
    have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance
    rcases ei.1 M with ⟨I, inj, f, monof⟩
    let T := ShortComplex.mk f (cokernel.π f) (cokernel.condition f)
    have T_exact : T.ShortExact := { exact := ShortComplex.exact_cokernel f }
    have T_exact' : Function.Exact (ConcreteCategory.hom T.f) (ConcreteCategory.hom T.g) :=
      (ShortComplex.ShortExact.moduleCat_exact_iff_function_exact _).mp T_exact.1
    have TS_exact' := IsLocalizedModule.map_exact S (T.X₁.localizedModuleMkLinearMap S)
      (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) _ _ T_exact'
    let TS := T.map (ModuleCat.localizedModuleFunctor S)
    have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
    let _ := (T_exact.hasInjectiveDimensionLT_X₃_iff n ‹_›).mpr ‹_›
    let _ : Injective TS.X₂ := (ModuleCat.localizedModuleFunctor.{v} S).injective_obj _
    exact (TS_exact.hasInjectiveDimensionLT_X₃_iff n ‹_›).mp (ih T.X₃)

Premises used: CategoryTheory.HasInjectiveDimensionLE, zero_add, Module.injective_iff_injective_object, CategoryTheory.injective_iff_hasInjectiveDimensionLT_one
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
M : ModuleCat.{v, u} R
n : ℕ
simp : HasInjectiveDimensionLE M n → HasInjectiveDimensionLE (M.localizedModule S) n
⊢ injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)

Tactic:
simp only [injectiveDimension_le_iff]

Premises used: CategoryTheory.injectiveDimension_le_iff
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
S : Submonoid R
M : ModuleCat.{v, u} R
n : ℕ
h : HasInjectiveDimensionLE M n
⊢ HasInjectiveDimensionLE (M.localizedModule S) n

Tactic:
M.localizedModule_hasInjectiveDimensionLE n S

Premises used: ModuleCat.localizedModule_hasInjectiveDimensionLE