awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⋯)
k : ℕ
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]))
right :
  LE.le (α := Multiset (Fin n))
    (degrees.{u_2, 0} (R := R)
      (Polynomial.coeff
        ((MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (C.g j)) k))
    ((Finsupp.toMultiset : (a : Fin n →₀ ℕ) → Multiset (Fin n))
      (Finsupp.comapDomain Fin.succ ((Multiset.toFinsupp : (a : Multiset (Fin (n + 1))) → Fin (n + 1) →₀ ℕ) d) ⋯))
⊢ degrees.{u_2, 0} (R := R)
      (Polynomial.coeff
        ((MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (C.g j))
        k) ≤
    B

Tactic:
simp only [B]
-- 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) ⋯)
k : ℕ
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]))
⊢ C.g j ∈ (↑(Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)) : Set (MvPolynomial (Fin (n + 1)) R))

Tactic:
replace hS := (hS _ hxS j).2
-- 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
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) ⋯)
k : ℕ
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]))
hS : C.g j ∈ (↑(Submodule.restrictScalars ℤ (degreesLE R (Fin (n + 1)) d)) : Set (MvPolynomial (Fin (n + 1)) R))
right :
  ∀ (hS : ∀ (a : Fin (n + 1)), degreeOf a (C.g j) ≤ Multiset.count a d) (a : Fin n),
    degreeOf.{u_2, 0} (R := R) a
        (Polynomial.coeff
          ((MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (C.g j))
          k) ≤
      Multiset.count a.succ d
⊢ LE.le (α := Multiset (Fin n))
    (degrees.{u_2, 0} (R := R)
      (Polynomial.coeff
        ((MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (C.g j)) k))
    ((Finsupp.toMultiset : (a : Fin n →₀ ℕ) → Multiset (Fin n))
      (Finsupp.comapDomain Fin.succ ((Multiset.toFinsupp : (a : Multiset (Fin (n + 1))) → Fin (n + 1) →₀ ℕ) d) ⋯))

Tactic:
simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, mem_degreesLE,
            Multiset.le_iff_count, Finsupp.count_toMultiset, Finsupp.comapDomain_apply,
            Multiset.toFinsupp_apply, ← degreeOf_def] at hS ⊢

Premises used: Multiset.le_iff_count, MvPolynomial.degreeOf_def, Multiset.toFinsupp_apply, Submodule.coe_restrictScalars, Finsupp.count_toMultiset, Finsupp.comapDomain_apply, MvPolynomial.mem_degreesLE, SetLike.mem_coe
-- 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
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) ⋯)
k : ℕ
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]))
hS : ∀ (a : Fin (n + 1)), degreeOf a (C.g j) ≤ Multiset.count a d
a : Fin n
⊢ degreeOf.{u_2, 0} (R := R) a
      (Polynomial.coeff
        ((MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (C.g j))
        k) ≤
    Multiset.count a.succ d

Tactic:
(degreeOf_coeff_finSuccEquiv (C.g j) a k).trans (hS _)

Premises used: MvPolynomial.degreeOf_coeff_finSuccEquiv, PrimeSpectrum.BasicConstructibleSetData.g, LE.le.trans
-- 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
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) ⋯)
k : ℕ
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]))
hS : ∀ (a : Fin (n + 1)), degreeOf a (C.g j) ≤ Multiset.count a d
a : Fin n
⊢ degreeOf.{u_2, 0} (R := R) a
      (Polynomial.coeff
        ((MvPolynomial.finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (C.g j))
        k) ≤
    Multiset.count a.succ d

Tactic:
exact (degreeOf_coeff_finSuccEquiv (C.g j) a k).trans (hS _)

Premises used: MvPolynomial.degreeOf_coeff_finSuccEquiv, PrimeSpectrum.BasicConstructibleSetData.g, LE.le.trans
-- 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))
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)

Tactic:
SetLike.le_def.mp ?_ ((hT₂ C hCT).2 a)

Premises used: SetLike.le_def, And.right, Iff.mp
-- 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))
C : BasicConstructibleSetData (MvPolynomial (Fin n) R)
hCT : C ∈ T
a : Fin C.n
refine :
  HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R))
      (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) (S'.degBound ^ S'.degBound) ≤
    coeffsIn (Fin n) (M ^ N) ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))
⊢ Membership.mem (γ := Submodule ℤ (MvPolynomial (Fin n) R))
    (coeffsIn (Fin n) (M ^ N) ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))) (C.g a)

Tactic:
refine SetLike.le_def.mp ?_ ((hT₂ C hCT).2 a)

Premises used: SetLike.le_def, And.right, Iff.mp
-- 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))
C : BasicConstructibleSetData (MvPolynomial (Fin n) R)
hCT : C ∈ T
a : Fin C.n
⊢ HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R))
      (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) (S'.degBound ^ S'.degBound) ≤
    coeffsIn (Fin n) (M ^ N) ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))

Tactic:
pow_inf_le.trans (inf_le_inf ?_ ?_)

Premises used: inf_le_inf, Set.Mem, Finsupp.onFinset, AddMonoidAlgebra.addAddCommGroup._aux_6, LE.le.trans, Finsupp.mapRange, pow_inf_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
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))
C : BasicConstructibleSetData (MvPolynomial (Fin n) R)
hCT : C ∈ T
a : Fin C.n
refine_1 :
  HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R)) (coeffsIn (Fin n) M) (S'.degBound ^ S'.degBound) ≤
    coeffsIn (Fin n) (M ^ N)
refine_2 :
  HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R)) (Submodule.restrictScalars ℤ (degreesLE R (Fin n) B))
      (S'.degBound ^ S'.degBound) ≤
    Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))
⊢ HPow.hPow (α := Submodule ℤ (MvPolynomial (Fin n) R))
      (coeffsIn (Fin n) M ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) B)) (S'.degBound ^ S'.degBound) ≤
    coeffsIn (Fin n) (M ^ N) ⊓ Submodule.restrictScalars ℤ (degreesLE R (Fin n) (N • B))

Tactic:
refine pow_inf_le.trans (inf_le_inf ?_ ?_)

Premises used: inf_le_inf, LE.le.trans, pow_inf_le