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
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)
injp : ∀ (m : MaximalSpectrum R), Injective (Sp m).X₂
⊢ (∀ (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)

Tactic:
(forall_congr' (fun p ↦ (Sp_exact p).hasInjectiveDimensionLT_X₃_iff n (injp p)))

Premises used: forall_congr', 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)
injp : ∀ (m : MaximalSpectrum R), Injective (Sp m).X₂
⊢ (∀ (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)

Tactic:
exact (forall_congr' (fun p ↦ (Sp_exact p).hasInjectiveDimensionLT_X₃_iff n (injp p)))

Premises used: forall_congr', 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 : ℕ
M : ModuleCat.{v, u} R
⊢ HasInjectiveDimensionLE M n ↔
    ∀ (p : PrimeSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl) n

Tactic:
⟨fun _ p ↦ M.localizedModule_hasInjectiveDimensionLE n p.1.primeCompl,
    fun h ↦ (M.hasInjectiveDimensionLE_iff_forall_maximalSpectrum n).mpr
    fun m ↦ h ⟨m.1, Ideal.IsMaximal.isPrime' m.1⟩⟩

Premises used: MaximalSpectrum.asIdeal, Iff.mpr, PrimeSpectrum.mk, ModuleCat.hasInjectiveDimensionLE_iff_forall_maximalSpectrum, Iff.intro, Ideal.primeCompl, PrimeSpectrum.asIdeal, ModuleCat.localizedModule_hasInjectiveDimensionLE, Ideal.IsMaximal.isPrime'
-- 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
n : ℕ
simp :
  HasInjectiveDimensionLE M n ↔
    ∀ (i : PrimeSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n
⊢ injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑n : WithBot ℕ∞)

Tactic:
simp only [injectiveDimension_le_iff, iSup_le_iff]

Premises used: CategoryTheory.injectiveDimension_le_iff, iSup_le_iff
-- 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
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔
    ∀ (i : PrimeSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
M.hasInjectiveDimensionLE_iff_forall_primeSpectrum n

Premises used: ModuleCat.hasInjectiveDimensionLE_iff_forall_primeSpectrum
-- 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
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔
    ∀ (i : PrimeSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
exact M.hasInjectiveDimensionLE_iff_forall_primeSpectrum n

Premises used: ModuleCat.hasInjectiveDimensionLE_iff_forall_primeSpectrum
-- 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
⊢ ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)

Tactic:
have aux (n : ℕ) : injectiveDimension M ≤ n ↔ ⨆ (p : PrimeSpectrum R), injectiveDimension
    (M.localizedModule p.1.primeCompl) ≤ n := by
    simp only [injectiveDimension_le_iff, iSup_le_iff]
    exact M.hasInjectiveDimensionLE_iff_forall_primeSpectrum n
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ injectiveDimension M =
    ⨆ (p : PrimeSpectrum R),
      injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)

Tactic:
eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
refine :
  ∀ (N : WithBot ℕ∞),
    injectiveDimension M ≤ N ↔
      ⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl) ≤
        N
⊢ injectiveDimension M =
    ⨆ (p : PrimeSpectrum R),
      injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)

Tactic:
refine eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
bot :
  Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
⊢ injectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥

Tactic:
simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, 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, iSup_eq_bot
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))

Tactic:
⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩

Premises used: LocalizedModule.instSubsingleton, Iff.intro, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
bot :
  ∀ (h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
    Subsingleton.{v + 1} (↑M : Type v)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))

Tactic:
refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
bot : ∀ (P : Ideal R) [inst_3 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑M : Type v))
⊢ Subsingleton.{v + 1} (↑M : Type v)

Tactic:
apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)

Premises used: Module.subsingleton_of_localization_maximal, LocalizedModule, ModuleCat.carrier, LocalizedModule.mkLinearMap, 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
h ⟨p, hp.isPrime⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule.{u, v} p.primeCompl (↑M : Type v))

Tactic:
exact h ⟨p, hp.isPrime⟩

Premises used: PrimeSpectrum.mk, Ideal.IsMaximal.isPrime
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : 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
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
n : ℕ
⊢ injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑(↑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
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
coe :
  injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)
coe₁ :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑(↑n : ℕ∞) : WithBot ℕ∞)
⊢ injectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑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
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot :
  injectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
coe :
  ∀ (N : ℕ∞),
    injectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
      ⨆ (p : PrimeSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl) ≤
        (↑N : WithBot ℕ∞)
⊢ injectiveDimension M ≤ N ↔
    ⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N

Tactic:
induction N with
  | bot =>
    simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp.isPrime⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Premises used: le_bot_iff, ModuleCat.isZero_iff_subsingleton, Module.subsingleton_of_localization_maximal, LocalizedModule, Equiv.subsingleton_congr, ModuleCat.carrier, CategoryTheory.injectiveDimension_eq_bot_iff, LocalizedModule.mkLinearMap, Ideal.primeCompl, ModuleCat.localizedModule, equivShrink, iSup_eq_bot
-- 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
n : ℕ
simp :
  HasInjectiveDimensionLE M n ↔
    ∀ (i : MaximalSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n
⊢ injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (m : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
          (M.localizedModule m.asIdeal.primeCompl))
      (↑n : WithBot ℕ∞)

Tactic:
simp only [injectiveDimension_le_iff, iSup_le_iff]

Premises used: CategoryTheory.injectiveDimension_le_iff, iSup_le_iff
-- 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
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔
    ∀ (i : MaximalSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
M.hasInjectiveDimensionLE_iff_forall_maximalSpectrum n

Premises used: ModuleCat.hasInjectiveDimensionLE_iff_forall_maximalSpectrum
-- 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
n : ℕ
⊢ HasInjectiveDimensionLE M n ↔
    ∀ (i : MaximalSpectrum R),
      HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
        (M.localizedModule i.asIdeal.primeCompl) n

Tactic:
exact M.hasInjectiveDimensionLE_iff_forall_maximalSpectrum n

Premises used: ModuleCat.hasInjectiveDimensionLE_iff_forall_maximalSpectrum
-- 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
⊢ ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)

Tactic:
have aux (n : ℕ) : injectiveDimension M ≤ n ↔ ⨆ (m : MaximalSpectrum R), injectiveDimension
    (M.localizedModule m.1.primeCompl) ≤ n := by
    simp only [injectiveDimension_le_iff, iSup_le_iff]
    exact M.hasInjectiveDimensionLE_iff_forall_maximalSpectrum n
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ injectiveDimension M =
    ⨆ (p : MaximalSpectrum R),
      injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)

Tactic:
eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff
-- 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
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
refine :
  ∀ (N : WithBot ℕ∞),
    injectiveDimension M ≤ N ↔
      ⨆ (p : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl) ≤
        N
⊢ injectiveDimension M =
    ⨆ (p : MaximalSpectrum R),
      injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)

Tactic:
refine eq_of_forall_ge_iff (fun N ↦ ?_)

Premises used: eq_of_forall_ge_iff