-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_2
inst : CommRing R
n_1 n : ℕ
IH :
  ∀ {M : Submodule ℤ R} (hM : 1 ∈ M) (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R))
    (hSn : ∀ C ∈ S, C.n ≤ k)
    (hS :
      ∀ C ∈ S,
        ∀ (j : Fin C.n),
          Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin n) R))
            (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) d)) (C.g j)),
    ∃ (T : ConstructibleSetData R),
      comap MvPolynomial.C '' S.toSet = T.toSet ∧
        ∀ C ∈ T,
          C.n ≤ numBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧
            ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n
M : Submodule ℤ R
hM : 1 ∈ M
k_1 : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k_1
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin (n + 1)) R))
        (coeffsIn (Fin (n + 1)) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)) (C.g j)
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := MvPolynomial.finSuccEquiv R n
S' : ConstructibleSetData (MvPolynomial (Fin n) R)[X] := ConstructibleSetData.map e.toRingEquiv.toRingHom S
hS' : S'.degBound ≤ k_1 * (1 + Multiset.count 0 d)
B : Multiset (Fin n) :=
  (Finsupp.toMultiset : (a : Fin n →₀ ℕ) → Multiset (Fin n))
    (Finsupp.comapDomain Fin.succ ((Multiset.toFinsupp : (a : Multiset (Fin (n + 1))) → Fin (n + 1) →₀ ℕ) d) ⋯)
x : BasicConstructibleSetData (MvPolynomial (Fin n) R)[X]
j : Fin x.n
k : ℕ
hxS :
  ∃ a ∈ S,
    { f := (MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) a.f,
        n := a.n,
        g :=
          (⇑(MvPolynomial.finSuccEquiv R n) : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) ∘
            a.g } =
      x
obtain :
  ∀ (C : BasicConstructibleSetData (MvPolynomial (Fin (n + 1)) R)) (hxS : C ∈ S)
    (j :
      Fin
        (BasicConstructibleSetData.n (R := (MvPolynomial (Fin n) R)[X])
          ({
              f :=
                (MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) C.f,
              n := C.n,
              g :=
                (⇑(MvPolynomial.finSuccEquiv R n) : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) ∘
                  C.g } :
            BasicConstructibleSetData (MvPolynomial (Fin n) R)[X]))),
    Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin n) R))
      (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B))
      (Polynomial.coeff
        (BasicConstructibleSetData.g
          { f := (MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) C.f,
            n := C.n,
            g :=
              (⇑(MvPolynomial.finSuccEquiv R n) : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) ∘
                C.g }
          j)
        k)
⊢ Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin n) R))
    (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) ((x.g j).coeff k)

Tactic:
obtain ⟨C, hxS, rfl⟩ := hxS

Premises used: rfl