Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
suppQ : Module.support R (Shrink.{v, u} (R ⧸ I)) = PrimeSpectrum.zeroLocus ↑I
tfae_1_to_2 :
  (∀ (N : ModuleCat R),
      Nontrivial ↑N →
        Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i)) →
    ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i)
tfae_2_to_3 :
  (∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i)) →
    ∃ N,
      Nontrivial ↑N ∧
        Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i)
tfae_3_to_4 :
  (∃ N,
      Nontrivial ↑N ∧
        Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i)) →
    ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
⊢ [∀ (N : ModuleCat R),
        Nontrivial ↑N →
          Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i),
      ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i),
      ∃ N,
        Nontrivial ↑N ∧
          Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i),
      ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE

Tactic:
tfae_have 4 → 1 := fun ⟨rs, len, mem, reg⟩ N Nntr Nfin Nsupp i hi ↦
    subsingleton_ext_of_exists_isRegular I N Nsupp M smul_lt rs mem reg i (hi.trans_eq len.symm)

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
ntrQ : Nontrivial (R ⧸ I)
suppQ : Module.support R (Shrink.{v, u} (R ⧸ I)) = PrimeSpectrum.zeroLocus ↑I
tfae_1_to_2 :
  (∀ (N : ModuleCat R),
      Nontrivial ↑N →
        Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i)) →
    ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i)
tfae_2_to_3 :
  (∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i)) →
    ∃ N,
      Nontrivial ↑N ∧
        Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i)
tfae_3_to_4 :
  (∃ N,
      Nontrivial ↑N ∧
        Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i)) →
    ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs
tfae_4_to_1 :
  (∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs) →
    ∀ (N : ModuleCat R),
      Nontrivial ↑N →
        Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i)
⊢ [∀ (N : ModuleCat R),
        Nontrivial ↑N →
          Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (Ext N M i),
      ∀ i < n, Subsingleton (Ext (of R (Shrink.{v, u} (R ⧸ I))) M i),
      ∃ N,
        Nontrivial ↑N ∧
          Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (Ext N M i),
      ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE