awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
rw :
  (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) ^
        (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) *
      ((numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) ^
          (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) *
        degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n)
⊢ degBound k₀ (fun (t : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) t k D) (n + 1 + 1) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
rw [degBound_succ, numBound_casesOn_succ, degBound_casesOn_succ, numBound_succ, degBound_succ,
      numBound_succ]

Premises used: ChevalleyThm.MvPolynomialC.numBound_succ, ChevalleyThm.MvPolynomialC.degBound_succ
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) ^
        (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
          ((k₀ * k) ^ (k₀ * k) • D) n) *
      ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) =
    (k₀ * k) ^ (k₀ * k) *
      ((numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) ^
          (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
            ((k₀ * k) ^ (k₀ * k) • D) n) *
        degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n)

Tactic:
ring
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₀ k : ℕ
D : ℕ → ℕ
⊢ numBound k₀ (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) x k D) (HAdd.hAdd (α := ℕ) 0 1) =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
rw :
  HMul.hMul (β := ℕ)
      (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
        ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n))
      (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) k D : ℕ) =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
      ((k₀ * k) ^ (k₀ * k) • D) n
⊢ numBound k₀ (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) x k D) (n + 1 + 1) =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
rw [numBound_succ (n := n + 1), numBound_casesOn_succ k₀ k D n, numBound_succ,
      degBound_casesOn_succ]

Premises used: ChevalleyThm.MvPolynomialC.numBound_succ, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
dsimp :
  numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
        ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) *
      D n =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
      ((k₀ * k) ^ (k₀ * k) * D n)
⊢ HMul.hMul (β := ℕ)
      (numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
        ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n))
      (Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ) (n + 1) k D : ℕ) =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
      ((k₀ * k) ^ (k₀ * k) • D) n

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
        ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) *
      D n =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
      ((k₀ * k) ^ (k₀ * k) * D n)

Tactic:
ring
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
hD : ∀ i < 0, D₁ i ≤ D₂ i
⊢ degBound k₁ D₁ 0 ≤ degBound k₂ D₂ 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
rw :
  numBound k₁ D₁ (n + 1) ^ numBound k₁ D₁ (n + 1) * degBound k₁ D₁ n ≤
    numBound k₂ D₂ (n + 1) ^ numBound k₂ D₂ (n + 1) * degBound k₂ D₂ n
⊢ degBound k₁ D₁ (n + 1) ≤ degBound k₂ D₂ (n + 1)

Tactic:
rw [degBound_succ, degBound_succ]

Premises used: ChevalleyThm.MvPolynomialC.degBound_succ
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ (n + 1) ^ numBound k₁ D₁ (n + 1) * degBound k₁ D₁ n ≤
    numBound k₂ D₂ (n + 1) ^ numBound k₂ D₂ (n + 1) * degBound k₂ D₂ n

Tactic:
Nat.mul_le_mul (Nat.pow_self_mono (numBound_mono hk _ hD)) (degBound_le_degBound hk _
      fun i hi ↦ hD _ (hi.trans n.lt_succ_self))

Premises used: Nat.lt_succ_self, Nat.mul_le_mul, LT.lt.trans, Nat.pow_self_mono
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ (n + 1) ^ numBound k₁ D₁ (n + 1) * degBound k₁ D₁ n ≤
    numBound k₂ D₂ (n + 1) ^ numBound k₂ D₂ (n + 1) * degBound k₂ D₂ n

Tactic:
refine Nat.mul_le_mul (Nat.pow_self_mono (numBound_mono hk _ hD)) (degBound_le_degBound hk _
      fun i hi ↦ hD _ (hi.trans n.lt_succ_self))

Premises used: Nat.lt_succ_self, Nat.mul_le_mul, LT.lt.trans, Nat.pow_self_mono
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
hD : ∀ i < 0, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ 0 ≤ numBound k₂ D₂ 0

Tactic:
simpa using hk
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
rw : numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ n * degBound k₂ D₂ n * D₂ n
⊢ numBound k₁ D₁ (n + 1) ≤ numBound k₂ D₂ (n + 1)

Tactic:
rw [numBound_succ, numBound_succ]

Premises used: ChevalleyThm.MvPolynomialC.numBound_succ
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
h₁ : numBound k₁ D₁ n ≤ numBound k₂ D₂ n
h₂ : degBound k₁ D₁ n ≤ degBound k₂ D₂ n
h₃ : D₁ n ≤ D₂ n
⊢ numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ n * degBound k₂ D₂ n * D₂ n

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ n ≤ numBound k₂ D₂ n

Tactic:
numBound_mono hk _ fun i hi ↦ hD _ (hi.trans n.lt_succ_self)

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ n ≤ numBound k₂ D₂ n

Tactic:
exact numBound_mono hk _ fun i hi ↦ hD _ (hi.trans n.lt_succ_self)

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ degBound k₁ D₁ n ≤ degBound k₂ D₂ n

Tactic:
degBound_le_degBound hk _ fun i hi ↦ hD _ (hi.trans n.lt_succ_self)

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ degBound k₁ D₁ n ≤ degBound k₂ D₂ n

Tactic:
exact degBound_le_degBound hk _ fun i hi ↦ hD _ (hi.trans n.lt_succ_self)

Premises used: Nat.lt_succ_self, LT.lt.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ D₁ n ≤ D₂ n

Tactic:
hD _ n.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ D₁ n ≤ D₂ n

Tactic:
exact hD _ n.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k : ℕ
D : ℕ → ℕ
⊢ 0 < degBound k D 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ 0 < degBound k D (n + 1)

Tactic:
simp [degBound_succ, Nat.pow_self_pos, degBound_pos]

Premises used: ChevalleyThm.MvPolynomialC.degBound_succ, Nat.pow_self_pos
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) 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)) 0 ∧
          ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0

Tactic:
⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩

Premises used: PrimeSpectrum.ConstructibleSetData.map, And.intro, RingEquiv.toRingHom, Exists.intro, MvPolynomial.isEmptyRingEquiv
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)) (C.g j)
zero :
  comap MvPolynomial.C '' S.toSet =
    (ConstructibleSetData.map (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) S).toSet
zero₁ :
  ∀ C ∈ ConstructibleSetData.map (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) S,
    C.n ≤ numBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0 ∧
      ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0
⊢ ∃ (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)) 0 ∧
          ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0

Tactic:
refine ⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)) (C.g j)
zero : comap MvPolynomial.C '' S.toSet = comap (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) ⁻¹' S.toSet
⊢ comap MvPolynomial.C '' S.toSet =
    (ConstructibleSetData.map (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) S).toSet

Tactic:
rw [ConstructibleSetData.toSet_map]

Premises used: PrimeSpectrum.ConstructibleSetData.toSet_map
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)) (C.g j)
zero :
  comap MvPolynomial.C '' S.toSet =
    Set.image (α := PrimeSpectrum (MvPolynomial (Fin 0) R))
      (⇑(comapEquiv (isEmptyRingEquiv R (Fin 0))) : (a : PrimeSpectrum (MvPolynomial (Fin 0) R)) → PrimeSpectrum R)
      S.toSet
⊢ comap MvPolynomial.C '' S.toSet =
    Set.preimage (β := PrimeSpectrum (MvPolynomial (Fin 0) R))
      (⇑(OrderIso.symm (comapEquiv (isEmptyRingEquiv R (Fin 0)))) :
        (a : PrimeSpectrum R) → PrimeSpectrum (MvPolynomial (Fin 0) R))
      S.toSet

Tactic:
rw [← OrderIso.image_eq_preimage_symm]

Premises used: OrderIso.image_eq_preimage_symm
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)) (C.g j)
⊢ comap MvPolynomial.C '' S.toSet =
    Set.image (α := PrimeSpectrum (MvPolynomial (Fin 0) R))
      (⇑(comapEquiv (isEmptyRingEquiv R (Fin 0))) : (a : PrimeSpectrum (MvPolynomial (Fin 0) R)) → PrimeSpectrum R)
      S.toSet

Tactic:
rfl
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)) (C.g j)
zero : ∀ a ∈ S, a.n ≤ k ∧ ∀ (i : Fin a.n), MvPolynomial.coeff 0 (a.g i) ∈ M
⊢ ∀ C ∈ ConstructibleSetData.map (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) S,
    C.n ≤ numBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0 ∧
      ∀ (i : Fin C.n), C.g i ∈ M ^ degBound k (fun (i : ℕ) ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) 0

Tactic:
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₂]

Premises used: ChevalleyThm.MvPolynomialC.numBound_zero, Finset.mem_image, and_imp, RingHom.coe_coe, forall_exists_index, PrimeSpectrum.ConstructibleSetData.map, pow_one, RingEquiv.toRingHom_eq_coe, Function.comp_apply, ChevalleyThm.MvPolynomialC.degBound_zero, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, forall_apply_eq_imp_iff₂, PrimeSpectrum.BasicConstructibleSetData.map
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)) (C.g j)
⊢ ∀ a ∈ S, a.n ≤ k ∧ ∀ (i : Fin a.n), MvPolynomial.coeff 0 (a.g i) ∈ M

Tactic:
fun a haS ↦ ⟨hSn a haS, fun i ↦ (hS a haS i).1 0⟩

Premises used: And.left, And.intro, OfNat.ofNat
-- 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 0)
S : ConstructibleSetData (MvPolynomial (Fin 0) R)
hSn : ∀ C ∈ S, C.n ≤ k
hS :
  ∀ C ∈ S,
    ∀ (j : Fin C.n),
      Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin 0) R))
        (coeffsIn (Fin 0) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin 0) d)) (C.g j)
⊢ ∀ a ∈ S, a.n ≤ k ∧ ∀ (i : Fin a.n), MvPolynomial.coeff 0 (a.g i) ∈ M

Tactic:
exact fun a haS ↦ ⟨hSn a haS, fun i ↦ (hS a haS i).1 0⟩
-- 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)
⊢ ∃ (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)

Tactic:
?_
-- 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
apply :
  ∀ (x : BasicConstructibleSetData (MvPolynomial (Fin n) R)[X]) (hxS : x ∈ S'),
    ∑ i : Fin x.n, (x.g i).degree.succ ≤ k * (1 + Multiset.count 0 d)
⊢ S'.degBound ≤ k * (1 + Multiset.count 0 d)

Tactic:
apply Finset.sup_le fun x hxS ↦ ?_

Premises used: Finset.sup_le
-- 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
x : BasicConstructibleSetData (MvPolynomial (Fin n) R)[X]
hxS : x ∈ S'
⊢ ∃ a ∈ S,
    { f := (e : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) a.f, n := a.n,
        g := (⇑e : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) ∘ a.g } =
      x

Tactic:
simp only [ConstructibleSetData.map, RingEquiv.toRingHom_eq_coe,
      AlgEquiv.toRingEquiv_toRingHom, Finset.mem_image, BasicConstructibleSetData.map,
      RingHom.coe_coe, S'] at hxS

Premises used: AlgEquiv.toRingEquiv_toRingHom, Finset.mem_image, RingHom.coe_coe, PrimeSpectrum.ConstructibleSetData.map, RingEquiv.toRingHom_eq_coe, PrimeSpectrum.BasicConstructibleSetData.map
-- 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
x : BasicConstructibleSetData (MvPolynomial (Fin n) R)[X]
hxS :
  ∃ a ∈ S,
    { f := (e : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) a.f, n := a.n,
        g := (⇑e : (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),
    ∑ i :
        Fin
          { f := (e : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) C.f, n := C.n,
              g := (⇑e : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) ∘ C.g }.n,
        (degree.{u_2} (R := MvPolynomial (Fin n) R)
            (BasicConstructibleSetData.g
              { f := (e : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) C.f, n := C.n,
                g := (⇑e : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) ∘ C.g }
              i)).succ ≤
      k * (1 + Multiset.count 0 d)
⊢ ∑ i : Fin x.n, (x.g i).degree.succ ≤ k * (1 + Multiset.count 0 d)

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

Premises used: rfl