awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R : Type u_6
inst : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
f : (C : BasicConstructibleSetData R[X]) → ConstructibleSetData R
hf₁ :
  ∀ (C : BasicConstructibleSetData R[X]),
    comap Polynomial.C '' (zeroLocus (Set.range { val := C.g : InductionObj R C.n }.val) \ zeroLocus {C.f}) =
      (f C).toSet
hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g : InductionObj R C.n }.degBound
hf₃ :
  ∀ (C : BasicConstructibleSetData R[X]),
    ∀ C_1 ∈ f C,
      ∀ (i : Fin C_1.n),
        C_1.g i ∈
          HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := C.g : InductionObj R C.n })
            { val := C.g : InductionObj R C.n }.powBound
x : BasicConstructibleSetData R
y : BasicConstructibleSetData R[X]
hy : y ∈ S
hx : x ∈ f y
H : { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound
i : Fin x.n
h : ¬S.degBound = 0
⊢ 1 ≤ S.degBound
have neg : S.degBound ≠ 0
Tactic: rwa [Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R : Type u_6
inst : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
have choose : ∀ (f : (C : BasicConstructibleSetData R[X]) → ConstructibleSetData R)
  (hf₁ :
    ∀ (C : BasicConstructibleSetData R[X]),
      comap Polynomial.C '' (zeroLocus (Set.range { val := C.g : InductionObj R C.n }.val) \ zeroLocus {C.f}) =
        (f C).toSet)
  (hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g : InductionObj R C.n }.degBound)
  (hf₃ :
    ∀ (C : BasicConstructibleSetData R[X]),
      ∀ C_1 ∈ f C,
        ∀ (i : Fin C_1.n),
          C_1.g i ∈
            HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := C.g : InductionObj R C.n })
              { val := C.g : InductionObj R C.n }.powBound),
  ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
Tactic: classical
  choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f
  refine ⟨S.biUnion f, ?_, ?_⟩
  · simp only [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.image_iUnion,
      Finset.set_biUnion_biUnion, hf₁]
  · simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
    intro x y hy hx
    have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
    refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
    gcongr
    · simpa [Submodule.one_eq_span]
    · refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
    · delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
R : Type u_6
inst : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
choose :
  ∀ (f : (C : BasicConstructibleSetData R[X]) → ConstructibleSetData R)
    (hf₁ :
      ∀ (C : BasicConstructibleSetData R[X]),
        comap Polynomial.C '' (zeroLocus (Set.range { val := C.g : InductionObj R C.n }.val) \ zeroLocus {C.f}) =
          (f C).toSet)
    (hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g : InductionObj R C.n }.degBound)
    (hf₃ :
      ∀ (C : BasicConstructibleSetData R[X]),
        ∀ C_1 ∈ f C,
          ∀ (i : Fin C_1.n),
            C_1.g i ∈
              HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := C.g : InductionObj R C.n })
                { val := C.g : InductionObj R C.n }.powBound),
    ∃ (T : ConstructibleSetData R),
      comap Polynomial.C '' S.toSet = T.toSet ∧
        ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
have refine_1 : ∀ (f : (C : BasicConstructibleSetData R[X]) → ConstructibleSetData R)
  (hf₁ :
    ∀ (C : BasicConstructibleSetData R[X]),
      comap Polynomial.C '' (zeroLocus (Set.range { val := C.g : InductionObj R C.n }.val) \ zeroLocus {C.f}) =
        (f C).toSet)
  (hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g : InductionObj R C.n }.degBound)
  (hf₃ :
    ∀ (C : BasicConstructibleSetData R[X]),
      ∀ C_1 ∈ f C,
        ∀ (i : Fin C_1.n),
          C_1.g i ∈
            HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := C.g : InductionObj R C.n })
              { val := C.g : InductionObj R C.n }.powBound),
  comap Polynomial.C '' S.toSet = ConstructibleSetData.toSet (Finset.biUnion S f)
Tactic: classical
  choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f
  refine ⟨S.biUnion f, ?_, ?_⟩
  · simp only [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.image_iUnion,
      Finset.set_biUnion_biUnion, hf₁]
  · simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
    intro x y hy hx
    have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
    refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
    gcongr
    · simpa [Submodule.one_eq_span]
    · refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
    · delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
k : ℕ
D : ℕ → ℕ
⊢ degBound k D 0 = 1
have rw : Eq (α := ℕ) 1 1
Tactic: rw [degBound]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
k : ℕ
D : ℕ → ℕ
⊢ numBound k D 0 = k
have rw : k = k
Tactic: rw [numBound]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ degBound k D (n + 1) = numBound k D (n + 1) ^ numBound k D (n + 1) * degBound k D n
have 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
Tactic: rw [degBound]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k D (n + 1) = numBound k D n * degBound k D n * D n
have rw : numBound k D n * degBound k D n * D n = numBound k D n * degBound k D n * D n
Tactic: rw [numBound]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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)
have 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)
Tactic: rw [degBound_succ, numBound_casesOn_succ, degBound_casesOn_succ, numBound_succ, degBound_succ,
      numBound_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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)
have 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
Tactic: rw [numBound_succ (n := n + 1), numBound_casesOn_succ k₀ k D n, numBound_succ,
      degBound_casesOn_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
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
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ degBound k₁ D₁ (n + 1) ≤ degBound k₂ D₂ (n + 1)
have 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
Tactic: rw [degBound_succ, degBound_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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)
have rw : numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ n * degBound k₂ D₂ n * D₂ n
Tactic: rw [numBound_succ, numBound_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
Goal:
k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ n * degBound k₂ D₂ n * D₂ n
have h₁ : numBound k₁ D₁ n ≤ numBound k₂ D₂ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ n * degBound k₂ D₂ n * D₂ n
have h₂ : degBound k₁ D₁ n ≤ degBound k₂ D₂ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ numBound k₁ D₁ n * degBound k₁ D₁ n * D₁ n ≤ numBound k₂ D₂ n * degBound k₂ D₂ n * D₂ n
have h₃ : D₁ n ≤ D₂ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
have zero : comap MvPolynomial.C '' S.toSet = (ConstructibleSetData.map (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) S).toSet
Tactic: refine ⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ ∃ (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
have 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
Tactic: refine ⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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 =
    (ConstructibleSetData.map (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) S).toSet
have zero : comap MvPolynomial.C '' S.toSet = comap (RingEquiv.toRingHom (isEmptyRingEquiv R (Fin 0))) ⁻¹' S.toSet
Tactic: rw [ConstructibleSetData.toSet_map]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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.preimage (β := PrimeSpectrum (MvPolynomial (Fin 0) R))
      (⇑(OrderIso.symm (comapEquiv (isEmptyRingEquiv R (Fin 0)))) :
        (a : PrimeSpectrum R) → PrimeSpectrum (MvPolynomial (Fin 0) R))
      S.toSet
have 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
Tactic: rw [← OrderIso.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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)
⊢ ∀ 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
have zero : ∀ a ∈ S, a.n ≤ k ∧ ∀ (i : Fin a.n), MvPolynomial.coeff 0 (a.g i) ∈ M
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₂]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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)
⊢ ∃ (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
have 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)
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 => ?_
Cleared hypotheses: M, hM, k, d, S, hSn, hS
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ S'.degBound ≤ k * (1 + Multiset.count 0 d)
have 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)
Tactic: apply Finset.sup_le fun x hxS ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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'
⊢ ∑ i : Fin x.n, (x.g i).degree.succ ≤ k * (1 + Multiset.count 0 d)
have 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
Tactic: simp only [ConstructibleSetData.map, RingEquiv.toRingHom_eq_coe,
      AlgEquiv.toRingEquiv_toRingHom, Finset.mem_image, BasicConstructibleSetData.map,
      RingHom.coe_coe, S'] at hxS
Cleared hypotheses: hxS