awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
have 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))
Tactic: have TS_exact' := IsLocalizedModule.map_exact S (T.X₁.localizedModuleMkLinearMap S)
      (T.X₂.localizedModuleMkLinearMap S) (T.X₃.localizedModuleMkLinearMap S) _ _ T_exact'
-- 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
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)
⊢ HasInjectiveDimensionLE (M.localizedModule S) (n + 1)
have TS_exact : TS.ShortExact
Tactic: have TS_exact : TS.ShortExact := T_exact.map_of_exact (ModuleCat.localizedModuleFunctor S)
-- 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
n : ℕ
S : Submonoid R
M : ModuleCat.{v, u} R
inst_3 : HasInjectiveDimensionLE M n
this : Small.{v, u} (Localization (M := R) S)
⊢ HasInjectiveDimensionLE (M.localizedModule S) n
have zero : ∀ (M : ModuleCat.{v, u} R) [HasInjectiveDimensionLE M 0], HasInjectiveDimensionLE (M.localizedModule S) 0
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₃)
Cleared hypotheses: n, M, inst_3
-- 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
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
⊢ HasInjectiveDimensionLE (M.localizedModule S) n
have 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)
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₃)
Cleared hypotheses: n, M, inst_3
-- 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
M : ModuleCat.{v, u} R
n : ℕ
⊢ injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
have simp : HasInjectiveDimensionLE M n → HasInjectiveDimensionLE (M.localizedModule S) n
Tactic: simp only [injectiveDimension_le_iff]
-- 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
M : ModuleCat.{v, u} R
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M
have aux : ∀ (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
-- 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
M : ModuleCat.{v, u} R
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M
have refine : ∀ (N : WithBot ℕ∞), injectiveDimension M ≤ N → injectiveDimension (M.localizedModule S) ≤ N
Tactic: refine le_of_forall_ge (fun N ↦ ?_)
-- 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
M : ModuleCat.{v, u} R
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
⊢ injectiveDimension M ≤ ⊥ → injectiveDimension (M.localizedModule S) ≤ ⊥
have bot : Subsingleton.{v + 1} (↑M : Type v) → Subsingleton (LocalizedModule.{u, v} S (↑M : Type v))
Tactic: simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
-- 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
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 ℕ∞)
have coe : injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑⊤ : WithBot ℕ∞)
Tactic: induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- 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
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 ℕ∞)
⊢ injectiveDimension M ≤ (↑N : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑N : WithBot ℕ∞)
have coe₁ : ∀ (n : ℕ),
  injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) →
    injectiveDimension (M.localizedModule S) ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)
Tactic: induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- 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
M : ModuleCat.{v, u} R
aux : ∀ (n : ℕ), injectiveDimension M ≤ (↑n : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
⊢ injectiveDimension M ≤ N → injectiveDimension (M.localizedModule S) ≤ N
have bot : injectiveDimension M ≤ ⊥ → injectiveDimension (M.localizedModule S) ≤ ⊥
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
Cleared hypotheses: N
-- 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
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) ≤ ⊥
⊢ injectiveDimension M ≤ N → injectiveDimension (M.localizedModule S) ≤ N
have coe : ∀ (N : ℕ∞), injectiveDimension M ≤ (↑N : WithBot ℕ∞) → injectiveDimension (M.localizedModule S) ≤ (↑N : WithBot ℕ∞)
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
Cleared hypotheses: N
-- 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
M : ModuleCat.{v, u} R
⊢ HasInjectiveDimensionLE M 0 ↔
    ∀ (m : MaximalSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl) 0
have zero : Injective M ↔
  ∀ (m : MaximalSpectrum R),
    Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
      (M.localizedModule m.asIdeal.primeCompl)
Tactic: simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]
-- 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
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)
have zero : ∀ (h : 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 ↦ ?_⟩
-- 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
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)
⊢ Injective M ↔
    ∀ (m : MaximalSpectrum R),
      Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)
have zero₁ : ∀
  (h :
    ∀ (m : MaximalSpectrum R),
      Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
        (M.localizedModule m.asIdeal.primeCompl)),
  Injective M
Tactic: refine ⟨fun h m ↦ ?_, fun h ↦ ?_⟩
-- 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
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) := ⋯
⊢ Injective (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
    (M.localizedModule m.asIdeal.primeCompl)
have zero : Module.Injective.{u, v} (Localization (M := R) m.asIdeal.primeCompl)
  (↑(M.localizedModule m.asIdeal.primeCompl) : Type v)
Tactic: rw [← Module.injective_iff_injective_object]
-- 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
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)
⊢ Injective M
have zero : Module.Injective.{u, v} R (↑M : Type v)
Tactic: rw [← Module.injective_iff_injective_object]
-- 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
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)
⊢ Module.Injective.{u, v} R (↑M : Type v)
have apply : ∀ (p : Ideal R) (hp : p.IsMaximal),
  Module.Injective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
Tactic: apply Module.injective_of_localization_maximal (fun p hp ↦ ?_)
-- 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
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 (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
have this₁ : 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⟩
-- 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
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)
⊢ Module.Injective (Localization.AtPrime p) (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))
have 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))
Tactic: rw [← Module.Baer.iff_injective] at this ⊢
Cleared hypotheses: this
-- 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 : ℕ
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
⊢ 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)
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
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)
⊢ 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)
have 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)
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
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) ⋯
⊢ 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)
have S_exact : S.ShortExact
Tactic: have S_exact : S.ShortExact := { exact := ShortComplex.exact_cokernel f }