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
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)
⊢ 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 Sp_exact : ∀ (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)
-- 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) ⋯
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 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 ih' : 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₃
-- 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)
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)
⊢ 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)
have 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)
Tactic: rw [← S_exact.hasInjectiveDimensionLT_X₃_iff n inj, ih']
-- 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) ⋯
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),
      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)
have injp : ∀ (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 _
-- 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 : ℕ
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
have zero : ∀ (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
Tactic: induction n generalizing M with
  | zero =>
    simp only [HasInjectiveDimensionLE, zero_add, ← injective_iff_hasInjectiveDimensionLT_one]
    refine ⟨fun h m ↦ ?_, fun h ↦ ?_⟩
    · let _ : Small.{v} (Localization m.1.primeCompl) :=
        small_of_surjective Localization.mkHom_surjective
      let _ : Module.Injective R M := Module.injective_module_of_injective_object R M
      rw [← Module.injective_iff_injective_object]
      exact Module.injective_of_isLocalizedModule m.1.primeCompl
        (M.localizedModuleMkLinearMap m.1.primeCompl)
    · rw [← Module.injective_iff_injective_object]
      apply Module.injective_of_localization_maximal (fun p hp ↦ ?_)
      let : Small.{v} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
      have : Module.Injective (Localization.AtPrime p) (M.localizedModule p.primeCompl) := by
        simpa [Module.injective_iff_injective_object] using h ⟨p, hp⟩
      rw [← Module.Baer.iff_injective] at this ⊢
      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
  | succ n ih =>
    have ei : EnoughInjectives (ModuleCat.{v} R) := inferInstance
    rcases ei.1 M with ⟨I, inj, f, monof⟩
    let S := ShortComplex.mk f (cokernel.π f) (cokernel.condition f)
    have S_exact : S.ShortExact := { exact := ShortComplex.exact_cokernel f }
    let Sp (m : MaximalSpectrum R) := S.map (ModuleCat.localizedModuleFunctor m.1.primeCompl)
    have Sp_exact (m : MaximalSpectrum R) : (Sp m).ShortExact :=
      S_exact.map_of_exact (ModuleCat.localizedModuleFunctor m.1.primeCompl)
    have ih' := ih S.X₃
    simp only [HasInjectiveDimensionLE] at ih' ⊢
    rw [← S_exact.hasInjectiveDimensionLT_X₃_iff n inj, ih']
    have injp (m : MaximalSpectrum R) : Injective (Sp m).X₂ :=
      (ModuleCat.localizedModuleFunctor.{v} m.1.primeCompl).injective_obj _
    exact (forall_congr' (fun p ↦ (Sp_exact p).hasInjectiveDimensionLT_X₃_iff n (injp p)))
Cleared hypotheses: n, M
-- 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
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 ℕ∞)
have simp : HasInjectiveDimensionLE M n ↔
  ∀ (i : PrimeSpectrum R),
    HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
      (M.localizedModule i.asIdeal.primeCompl) n
Tactic: simp only [injectiveDimension_le_iff, iSup_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
M : ModuleCat.{v, u} R
⊢ injectiveDimension M =
    ⨆ (p : PrimeSpectrum R),
      injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)
have 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 ℕ∞)
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
-- 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
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)
have 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
Tactic: refine eq_of_forall_ge_iff (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
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 ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
have bot : Subsingleton.{v + 1} (↑M : Type v) ↔
  ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
Tactic: simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, 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
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))
have bot : ∀ (h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
  Subsingleton.{v + 1} (↑M : Type v)
Tactic: refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, 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
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))
⊢ Subsingleton.{v + 1} (↑M : Type v)
have bot : ∀ (P : Ideal R) [inst_3 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑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)
-- 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
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 ℕ∞) ↔
    ⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
have 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 ℕ∞)
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
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 ℕ∞)
⊢ 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 ℕ∞)
have 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 ℕ∞)
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
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 ℕ∞
⊢ injectiveDimension M ≤ N ↔
    ⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have 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))
    ⊥
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
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
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))
      ⊥
⊢ injectiveDimension M ≤ N ↔
    ⨆ (p : PrimeSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have 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 ℕ∞)
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
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
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 ℕ∞)
have simp : HasInjectiveDimensionLE M n ↔
  ∀ (i : MaximalSpectrum R),
    HasInjectiveDimensionLE (C := ModuleCat.{v, u} (Localization (M := R) i.asIdeal.primeCompl))
      (M.localizedModule i.asIdeal.primeCompl) n
Tactic: simp only [injectiveDimension_le_iff, iSup_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
M : ModuleCat.{v, u} R
⊢ injectiveDimension M =
    ⨆ (p : MaximalSpectrum R),
      injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl)
have 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 ℕ∞)
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
-- 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
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)
have 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
Tactic: refine eq_of_forall_ge_iff (fun N ↦ ?_)