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

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)))

Premises used: Module.Baer.iff_injective, CategoryTheory.HasInjectiveDimensionLE, zero_add, Module.injective_iff_injective_object, CategoryTheory.injective_iff_hasInjectiveDimensionLT_one, Module.injective_of_localization_maximal