-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
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)
succ :
  ∀ (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)),
    ∃ (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 + 1) ∧
            ∀ (i : Fin C.n),
              C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) (n + 1)
⊢ ∃ (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

Tactic:
induction n generalizing k M with
  | zero =>
    refine ⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩
    · rw [ConstructibleSetData.toSet_map]
      change _ = (comapEquiv (isEmptyRingEquiv _ _)).symm ⁻¹' _
      rw [← OrderIso.image_eq_preimage_symm]
      rfl
    · simp only [ConstructibleSetData.map, RingEquiv.toRingHom_eq_coe, Finset.mem_image, comp_apply,
        BasicConstructibleSetData.map, RingHom.coe_coe, isEmptyRingEquiv_eq_coeff_zero, pow_one,
        numBound_zero, degBound_zero, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
      exact fun a haS ↦ ⟨hSn a haS, fun i ↦ (hS a haS i).1 0⟩
  | succ n IH => ?_

Premises used: ChevalleyThm.MvPolynomialC.numBound_zero, PrimeSpectrum.comapEquiv, Finset.mem_image, and_imp, RingHom.coe_coe, forall_exists_index, OrderIso.symm, PrimeSpectrum.ConstructibleSetData.map, pow_one, RingEquiv.toRingHom_eq_coe, Function.comp_apply, PrimeSpectrum.ConstructibleSetData.toSet_map, OrderIso.image_eq_preimage_symm, ChevalleyThm.MvPolynomialC.degBound_zero, MvPolynomial.isEmptyRingEquiv, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, forall_apply_eq_imp_iff₂, PrimeSpectrum.BasicConstructibleSetData.map