awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact M.localizedModule_hasInjectiveDimensionLE n S

Premises used: ModuleCat.localizedModule_hasInjectiveDimensionLE
-- 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 : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)

Tactic:
have aux (n : ℕ) : injectiveDimension M ≤ n → injectiveDimension (M.localizedModule S) ≤ n := by
    simp only [injectiveDimension_le_iff]
    intro h
    exact M.localizedModule_hasInjectiveDimensionLE n 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
M : ModuleCat.{v, u} R
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M

Tactic:
le_of_forall_ge (fun N ↦ ?_)

Premises used: le_of_forall_ge
-- 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
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
refine : ∀ (N : WithBot ℕ∞), injectiveDimension M ≤ N → injectiveDimension (M.localizedModule S) ≤ N
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M

Tactic:
refine le_of_forall_ge (fun N ↦ ?_)

Premises used: le_of_forall_ge
-- 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
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
bot : Subsingleton.{v + 1} (↑M : Type v) → Subsingleton (LocalizedModule.{u, v} S (↑M : Type v))
⊢ injectiveDimension M ≤ ⊥ → injectiveDimension (M.localizedModule S) ≤ ⊥

Tactic:
simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Equiv.subsingleton_congr, CategoryTheory.injectiveDimension_eq_bot_iff, ModuleCat.localizedModule, equivShrink
-- 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
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
h : Subsingleton.{v + 1} (↑M : Type v)
⊢ Subsingleton (LocalizedModule.{u, v} S (↑M : Type v))

Tactic:
apply LocalizedModule.instSubsingleton _

Premises used: LocalizedModule.instSubsingleton
-- 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
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
⊢ injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑⊤ : WithBot ℕ∞)

Tactic:
simp
-- 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
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
n : ℕ
⊢ injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) →
    injectiveDimension (M.localizedModule S) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)

Tactic:
simpa using aux n
-- 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
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
N : ℕ∞
coe : injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑⊤ : WithBot ℕ∞)
coe₁ :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) →
      injectiveDimension (M.localizedModule S) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)
⊢ injectiveDimension M ≤ (↑N : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑N : WithBot ℕ∞)

Tactic:
induction N with
    | top => simp
    | coe n => simpa using aux n
-- 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
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot : injectiveDimension M ≤ ⊥ → injectiveDimension (M.localizedModule S) ≤ ⊥
coe :
  ∀ (N : ℕ∞), injectiveDimension M ≤ (↑N : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑N : WithBot ℕ∞)
⊢ injectiveDimension M ≤ N → injectiveDimension (M.localizedModule S) ≤ N

Tactic:
induction N with
  | bot =>
    simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    intro _
    apply LocalizedModule.instSubsingleton _
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, LocalizedModule.instSubsingleton, Equiv.subsingleton_congr, CategoryTheory.injectiveDimension_eq_bot_iff, ModuleCat.localizedModule, equivShrink
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
zero :
  Injective M ↔
    ∀ (m : MaximalSpectrum R),
      Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)
⊢ HasInjectiveDimensionLE M 0 ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) 0

Tactic:
simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]

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
M : ModuleCat.{v, u} R
⊢ Injective M ↔
    ∀ (m : MaximalSpectrum R),
      Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)

Tactic:
⟨fun h m ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
zero :
  ∀ (h : Injective M) (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
zero₁ :
  ∀
    (h :
      ∀ (m : MaximalSpectrum R),
        Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl)),
    Injective M
⊢ Injective M ↔
    ∀ (m : MaximalSpectrum R),
      Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)

Tactic:
refine ⟨fun h m ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
h : Injective M
m : MaximalSpectrum R
h_1 : Small.{v, u} (Localization (M := R) m.asIdeal.primeCompl) := ⋯
h_2 : Module.Injective.{u, v} R (↑M : Type v) := ⋯
zero :
  Module.Injective.{u, v} (Localization (M := R) m.asIdeal.primeCompl)
    (↑(M.localizedModule m.asIdeal.primeCompl) : Type v)
⊢ Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
    (M.localizedModule m.asIdeal.primeCompl)

Tactic:
rw [← Module.injective_iff_injective_object]

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
M : ModuleCat.{v, u} R
h : Injective M
m : MaximalSpectrum R
h_1 : Small.{v, u} (Localization (M := R) m.asIdeal.primeCompl) := ⋯
h_2 : Module.Injective.{u, v} R (↑M : Type v) := ⋯
⊢ Module.Injective.{u, v} (Localization (M := R) m.asIdeal.primeCompl)
    (↑(M.localizedModule m.asIdeal.primeCompl) : Type v)

Tactic:
Module.injective_of_isLocalizedModule m.1.primeCompl
        (M.localizedModuleMkLinearMap m.1.primeCompl)

Premises used: MaximalSpectrum.asIdeal, ModuleCat.localizedModuleMkLinearMap, Module.injective_of_isLocalizedModule, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
h : Injective M
m : MaximalSpectrum R
h_1 : Small.{v, u} (Localization (M := R) m.asIdeal.primeCompl) := ⋯
h_2 : Module.Injective.{u, v} R (↑M : Type v) := ⋯
⊢ Module.Injective.{u, v} (Localization (M := R) m.asIdeal.primeCompl)
    (↑(M.localizedModule m.asIdeal.primeCompl) : Type v)

Tactic:
exact Module.injective_of_isLocalizedModule m.1.primeCompl
        (M.localizedModuleMkLinearMap m.1.primeCompl)

Premises used: MaximalSpectrum.asIdeal, ModuleCat.localizedModuleMkLinearMap, Module.injective_of_isLocalizedModule, Ideal.primeCompl
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
h :
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
zero : Module.Injective.{u, v} R (↑M : Type v)
⊢ Injective M

Tactic:
rw [← Module.injective_iff_injective_object]

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
M : ModuleCat.{v, u} R
h :
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
apply :
  ∀ (p : Ideal R) (hp : p.IsMaximal),
    Module.Injective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
⊢ Module.Injective.{u, v} R (↑M : Type v)

Tactic:
apply Module.injective_of_localization_maximal (fun p hp ↦ ?_)

Premises used: Module.injective_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
h :
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := ⋯
⊢ Module.Injective.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)

Tactic:
simpa [Module.injective_iff_injective_object] using h ⟨p, hp⟩

Premises used: MaximalSpectrum.mk, 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
M : ModuleCat.{v, u} R
h :
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this : Small.{v, u} (Localization.AtPrime p) := ⋯
⊢ Module.Injective.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)

Tactic:
have : Module.Injective (Localization.AtPrime p) (M.localizedModule p.primeCompl) := by
        simpa [Module.injective_iff_injective_object] using h ⟨p, hp⟩
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
h :
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this_1 : Small.{v, u} (Localization.AtPrime p) := ⋯
this : Module.Injective.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)
rw :
  ∀ (this : Module.Baer.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)),
    Module.Baer (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
⊢ Module.Injective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
rw [← Module.Baer.iff_injective] at this ⊢

Premises used: Module.Baer.iff_injective
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
h :
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this_1 : Small.{v, u} (Localization.AtPrime p) := ⋯
this : Module.Baer.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)
⊢ Module.Baer (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
Module.Baer.of_equiv (LinearEquiv.extendScalarsOfIsLocalization p.primeCompl
        (Localization.AtPrime p) (IsLocalizedModule.linearEquiv p.primeCompl
        (M.localizedModuleMkLinearMap p.primeCompl)
        (LocalizedModule.mkLinearMap p.primeCompl M))) this

Premises used: IsLocalizedModule.linearEquiv, Module.Baer.of_equiv, Localization.AtPrime, ModuleCat.localizedModuleMkLinearMap, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl, LinearEquiv.extendScalarsOfIsLocalization
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
h :
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this_1 : Small.{v, u} (Localization.AtPrime p) := ⋯
this : Module.Baer.{u, v} (Localization.AtPrime p) (↑(M.localizedModule p.primeCompl) : Type v)
⊢ Module.Baer (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
exact Module.Baer.of_equiv (LinearEquiv.extendScalarsOfIsLocalization p.primeCompl
        (Localization.AtPrime p) (IsLocalizedModule.linearEquiv p.primeCompl
        (M.localizedModuleMkLinearMap p.primeCompl)
        (LocalizedModule.mkLinearMap p.primeCompl M))) this

Premises used: IsLocalizedModule.linearEquiv, Module.Baer.of_equiv, Localization.AtPrime, ModuleCat.localizedModuleMkLinearMap, ModuleCat.carrier, LocalizedModule.mkLinearMap, Ideal.primeCompl, LinearEquiv.extendScalarsOfIsLocalization
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat.{v, u} R
⊢ 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
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat.{v, u} R
ei : EnoughInjectives (ModuleCat.{v, u} R)
succ :
  ∀ (I : ModuleCat.{v, u} R) (inj : Injective I) (f : M ⟶ I) (monof : Mono f),
    HasInjectiveDimensionLE M (n + 1) ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) (n + 1)
⊢ HasInjectiveDimensionLE M (n + 1) ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) (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
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat.{v, u} R
ei : EnoughInjectives (ModuleCat.{v, u} R)
I : ModuleCat.{v, u} R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
⊢ S.ShortExact

Tactic:
have S_exact : S.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
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat.{v, u} R
ei : EnoughInjectives (ModuleCat.{v, u} R)
I : ModuleCat.{v, u} R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl)) :=
  fun (m : MaximalSpectrum R) ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
⊢ ∀ (m : MaximalSpectrum R), (Sp m).ShortExact

Tactic:
have Sp_exact (m : MaximalSpectrum R) : (Sp m).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor m.1.primeCompl)
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat.{v, u} R
ei : EnoughInjectives (ModuleCat.{v, u} R)
I : ModuleCat.{v, u} R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl)) :=
  fun (m : MaximalSpectrum R) ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
⊢ HasInjectiveDimensionLE S.X₃ n ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (S.X₃.localizedModule m.asIdeal.primeCompl) n

Tactic:
have ih' := ih S.X₃
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat.{v, u} R
ei : EnoughInjectives (ModuleCat.{v, u} R)
I : ModuleCat.{v, u} R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl)) :=
  fun (m : MaximalSpectrum R) ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
ih' :
  HasInjectiveDimensionLT S.X₃ (n + 1) ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLT (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (S.X₃.localizedModule m.asIdeal.primeCompl) (n + 1)
succ :
  (∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLT (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (S.X₃.localizedModule m.asIdeal.primeCompl) (n + 1)) ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLT (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)
⊢ HasInjectiveDimensionLT M (n + 1 + 1) ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLT (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)

Tactic:
rw [← S_exact.hasInjectiveDimensionLT_X₃_iff n inj, ih']

Premises used: CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff
-- Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat.{v, u} R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R),
        HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat.{v, u} R
ei : EnoughInjectives (ModuleCat.{v, u} R)
I : ModuleCat.{v, u} R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat.{v, u} R) := ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl)) :=
  fun (m : MaximalSpectrum R) ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
ih' :
  HasInjectiveDimensionLT S.X₃ (n + 1) ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLT (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (S.X₃.localizedModule m.asIdeal.primeCompl) (n + 1)
⊢ ∀ (m : MaximalSpectrum R), Injective (Sp m).X₂

Tactic:
have injp (m : MaximalSpectrum R) : Injective (Sp m).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} m.1.primeCompl).injective_obj _