-- 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 : ℕ
d : Multiset (Fin (n + 1))
S : ConstructibleSetData (MvPolynomial (Fin (n + 1)) R)
hSn : ∀ C ∈ S, C.n ≤ k
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 + 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) ⋯)
T : ConstructibleSetData (MvPolynomial (Fin n) R)
hT₁ : comap Polynomial.C '' S'.toSet = T.toSet
hT₂ :
  ∀ C ∈ T,
    C.n ≤ S'.degBound ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R))
            (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) (S'.degBound ^ S'.degBound)
N : ℕ := (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d))
this_1 :
  ∀ (C : BasicConstructibleSetData (MvPolynomial (Fin n) R)) (hCT : C ∈ T) (a : Fin C.n),
    Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin n) R))
      (coeffsIn (Fin n) (M ^ N) ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))) (C.g a)
h1M : 1 ≤ M
U : ConstructibleSetData R
hU₁ : comap MvPolynomial.C '' T.toSet = U.toSet
hU₂ :
  ∀ C ∈ U,
    C.n ≤
        numBound S'.degBound
          (fun (i : ℕ) ↦
            1 +
              (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                Multiset.count i (Multiset.map Fin.val B))
          n ∧
      ∀ (i : Fin C.n),
        C.g i ∈
          M ^
            ((k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
              degBound S'.degBound
                (fun (i : ℕ) ↦
                  1 +
                    (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
                      Multiset.count i (Multiset.map Fin.val B))
                n)
this :
  ∀ i < n + 1,
    (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) i (1 + Multiset.count 0 d) fun (x : ℕ) ↦
        1 + Multiset.count x (Multiset.map Fin.val B)) ≤
      1 + Multiset.count i (Multiset.map Fin.val d)
C : BasicConstructibleSetData R
hCU : C ∈ U
i : Fin C.n
succ :
  ∀ x < n,
    1 + (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) * Multiset.count x (Multiset.map Fin.val B) ≤
      HSMul.hSMul (β := ℕ → ℕ) ((k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)))
        (fun (x : ℕ) ↦ 1 + Multiset.count x (Multiset.map Fin.val B)) x
⊢ (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) *
      degBound S'.degBound
        (fun (i : ℕ) ↦
          1 +
            (k * (1 + Multiset.count 0 d)) ^ (k * (1 + Multiset.count 0 d)) * Multiset.count i (Multiset.map Fin.val B))
        n ≤
    degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 1)

Tactic:
refine (Nat.mul_le_mul le_rfl (degBound_le_degBound hS' _ fun _ _ ↦ ?_)).trans
      ((degBound_casesOn_succ k _ _ _).symm.trans_le (degBound_le_degBound le_rfl _ this))

Premises used: ChevalleyThm.MvPolynomialC.degBound_casesOn_succ, le_rfl, Eq.trans_le, Nat.mul_le_mul, LE.le.trans, Eq.symm, ChevalleyThm.MvPolynomialC.degBound_le_degBound