-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_2
inst : CommRing R
m n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial (Fin m) R
k : ℕ
d : Multiset (Fin m)
S : ConstructibleSetData (MvPolynomial (Fin m) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS : ∀ C ∈ S, ∀ (j : Fin C.n), (C.g j).degrees ≤ d
hf :
  ∀ (i : Fin n),
    degrees.{u_2, 0} (R := R) ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) ≤ d
g : MvPolynomial (Fin m) (MvPolynomial (Fin n) R) →+* MvPolynomial (Fin m) R := eval₂Hom f.toRingHom MvPolynomial.X
hg :
  Eq (α := MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
    (g.comp (algebraMap (MvPolynomial (Fin n) R) (MvPolynomial (Fin m) (MvPolynomial (Fin n) R))))
    (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)
σ : MvPolynomial (Fin m) R →+* MvPolynomial (Fin m) (MvPolynomial (Fin n) R) :=
  MvPolynomial.map (algebraMap R (MvPolynomial (Fin n) R))
hσ : g.comp σ = RingHom.id (MvPolynomial (Fin m) R)
hσ' :
  ∀ (x : MvPolynomial (Fin m) R),
    (g : (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin m) R)
        ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) x) =
      x
hg' :
  Surjective (α := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (β := MvPolynomial (Fin m) R)
    (⇑g : (a : MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) → MvPolynomial (Fin m) R)
S' : ConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Finset.image
    (fun (x : BasicConstructibleSetData (MvPolynomial (Fin m) R)) ↦
      match (motive :=
        BasicConstructibleSetData (MvPolynomial (Fin m) R) →
          BasicConstructibleSetData (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))
        x with
      | { f := fk, n := k, g := gk } =>
        { f := (σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) fk, n := k + n,
          g := fun (s : Fin (k + n)) ↦
            Sum.elim ((⇑σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) ∘ gk)
              (fun (i : Fin n) ↦
                HSub.hSub (α := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (β :=
                  MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                  ((MvPolynomial.C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                      (MvPolynomial.X i) :
                    MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                  ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
                      ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) :
                    MvPolynomial (Fin m) (MvPolynomial (Fin n) R)))
              ((Equiv.symm finSumFinEquiv : (a : Fin (k + n)) → Fin k ⊕ Fin n) s) })
    S
s₀ : Set (MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) :=
  Set.range fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin m) (MvPolynomial (Fin n) R)) (β := MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
      ((MvPolynomial.C : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
          (MvPolynomial.X i) :
        MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
      ((σ : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
          ((f : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin m) R) (MvPolynomial.X i)) :
        MvPolynomial (Fin m) (MvPolynomial (Fin n) R))
hs : zeroLocus s₀ = Set.range (comap g)
hg'' : ∀ (t : Set (PrimeSpectrum (MvPolynomial (Fin m) R))), comap g '' t = comap σ ⁻¹' t ∩ zeroLocus s₀
hS' : comap g '' S.toSet = S'.toSet
obtain :
  ∀ (T : ConstructibleSetData (MvPolynomial (Fin n) R)) (hT : comap MvPolynomial.C '' S'.toSet = T.toSet)
    (hT' :
      ∀ C ∈ T,
        C.n ≤ MvPolynomialC.numBound (k + n) (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) m ∧
          ∀ (i : Fin C.n),
            C.g i ∈
              HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R))
                (Submodule.restrictScalars ℤ (degreesLE R (Fin n) (Finset.val Finset.univ)))
                (MvPolynomialC.degBound (k + n) (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) m)),
    ∃ (T : ConstructibleSetData (MvPolynomial (Fin n) R)),
      Eq (α := Set (PrimeSpectrum (MvPolynomial (Fin n) R)))
          (Set.image (α := PrimeSpectrum (MvPolynomial (Fin m) R))
            (comap (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)) S.toSet)
          T.toSet ∧
        ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d
⊢ ∃ (T : ConstructibleSetData (MvPolynomial (Fin n) R)),
    Eq (α := Set (PrimeSpectrum (MvPolynomial (Fin n) R)))
        (Set.image (α := PrimeSpectrum (MvPolynomial (Fin m) R))
          (comap (↑f : MvPolynomial (Fin n) R →+* MvPolynomial (Fin m) R)) S.toSet)
        T.toSet ∧
      ∀ C ∈ T, C.n ≤ numBound k m n d ∧ ∀ (i : Fin C.n) (j : Fin n), degreeOf j (C.g i) ≤ degBound k m n d

Tactic:
obtain ⟨T, hT, hT'⟩ :=
    chevalley_mvPolynomialC
    (M := (degreesLE R (Fin n) Finset.univ.1).restrictScalars ℤ) (by simp) (k + n) d S'
    (Finset.forall_mem_image.mpr fun x hx ↦ (by simpa using hSn _ hx))
    (Finset.forall_mem_image.mpr fun x hx ↦ by
      intro j
      obtain ⟨j, rfl⟩ := finSumFinEquiv.surjective j
      simp only [Equiv.symm_apply_apply, Submodule.mem_inf, mem_coeffsIn,
        Submodule.restrictScalars_mem, mem_degreesLE]
      constructor
      · intro i
        obtain j | j := j
        · simp [σ, MvPolynomial.coeff_map, degrees_C]
        · simp only [MvPolynomial.algebraMap_eq, Sum.elim_inr, MvPolynomial.coeff_sub,
            MvPolynomial.coeff_C, MvPolynomial.coeff_map, σ]
          refine degrees_sub_le.trans ?_
          simp only [degrees_C, apply_ite, degrees_zero,
            Multiset.union_zero]
          split_ifs with h
          · refine (degrees_X' _).trans ?_
            simp
          · simp
      · obtain j | j := j
        · simp only [MvPolynomial.algebraMap_eq, Sum.elim_inl, comp_apply, σ]
          exact degrees_map_le.trans (hS _ hx j)
        · refine degrees_sub_le.trans ?_
          simp only [degrees_C, Multiset.zero_union]
          exact degrees_map_le.trans (hf _))

Premises used: Iff.mpr, ChevalleyThm.chevalley_mvPolynomialC, Finset.forall_mem_image, HAdd.hAdd