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
⊢ ∃ (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: choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f
-- 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
⊢ ∃ (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 : comap Polynomial.C '' S.toSet = ConstructibleSetData.toSet (Finset.biUnion S f)
Tactic: refine ⟨S.biUnion f, ?_, ?_⟩
-- 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
refine_1 : comap Polynomial.C '' S.toSet = ConstructibleSetData.toSet (Finset.biUnion S f)
⊢ ∃ (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_2 : ∀ C ∈ Finset.biUnion S f, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
Tactic: refine ⟨S.biUnion f, ?_, ?_⟩
-- 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
⊢ ∀ C ∈ Finset.biUnion S f, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
have refine_2 : ∀ (C : BasicConstructibleSetData R),
  ∀ x ∈ S, C ∈ f x → C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
Tactic: simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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
⊢ x.n ≤ S.degBound ∧ ∀ (i : Fin x.n), x.g i ∈ M ^ S.degBound ^ S.degBound
have H : { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound
Tactic: have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
-- 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
⊢ x.n ≤ S.degBound ∧ ∀ (i : Fin x.n), x.g i ∈ M ^ S.degBound ^ S.degBound
have refine_2 : ∀ (i : Fin x.n),
  HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := y.g : InductionObj R y.n })
      { val := y.g : InductionObj R y.n }.powBound ≤
    M ^ S.degBound ^ S.degBound
Tactic: refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
-- 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
⊢ HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := y.g : InductionObj R y.n })
      { val := y.g : InductionObj R y.n }.powBound ≤
    M ^ S.degBound ^ S.degBound
have refine_2 : 1 ≤ M
Tactic: gcongr
-- 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
refine_2 : 1 ≤ M
⊢ HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := y.g : InductionObj R y.n })
      { val := y.g : InductionObj R y.n }.powBound ≤
    M ^ S.degBound ^ S.degBound
have refine_2₁ : coeffSubmodule ℤ { val := y.g : InductionObj R y.n } ≤ M
Tactic: gcongr
-- 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
refine_2 : 1 ≤ M
refine_2₁ : coeffSubmodule ℤ { val := y.g : InductionObj R y.n } ≤ M
⊢ HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := y.g : InductionObj R y.n })
      { val := y.g : InductionObj R y.n }.powBound ≤
    M ^ S.degBound ^ S.degBound
have refine_2₂ : { val := y.g : InductionObj R y.n }.powBound ≤ S.degBound ^ S.degBound
Tactic: gcongr
-- 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
⊢ coeffSubmodule ℤ { val := y.g : InductionObj R y.n } ≤ M
have refine_2 : {1} ∪ ⋃ (i : Fin y.n), Set.range ({ val := y.g : InductionObj R y.n }.val i).coeff ⊆ (↑M : Set R)
Tactic: refine Submodule.span_le.mpr ?_
-- 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
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
have pos : ∀ (h : S.degBound = 0),
  { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
Tactic: by_cases h : S.degBound = 0
-- 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
pos :
  ∀ (h : S.degBound = 0),
    { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤
      S.degBound ^ S.degBound
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
have neg : ∀ (h : ¬S.degBound = 0),
  { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
Tactic: by_cases h : S.degBound = 0
-- 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
⊢ { val := y.g : InductionObj R y.n }.degBound = 0
have nlinarith : { val := y.g : InductionObj R y.n }.degBound < 0 →
  -1 + HSub.hSub (α := ℤ) 0 (↑{ val := y.g : InductionObj R y.n }.degBound : ℤ) +
      (HAdd.hAdd (α := ℤ) (↑{ val := y.g : InductionObj R y.n }.degBound : ℤ) 1 - 0) =
    0
Tactic: nlinarith
-- 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
nlinarith :
  { val := y.g : InductionObj R y.n }.degBound < 0 →
    -1 + HSub.hSub (α := ℤ) 0 (↑{ val := y.g : InductionObj R y.n }.degBound : ℤ) +
        (HAdd.hAdd (α := ℤ) (↑{ val := y.g : InductionObj R y.n }.degBound : ℤ) 1 - 0) =
      0
⊢ { val := y.g : InductionObj R y.n }.degBound = 0
have nlinarith₁ : 0 < { val := y.g : InductionObj R y.n }.degBound →
  -1 + HSub.hSub (α := ℤ) (↑{ val := y.g : InductionObj R y.n }.degBound : ℤ) (↑S.degBound : ℤ) +
        HSub.hSub (α := ℤ) (↑S.degBound : ℤ) 0 +
      (HAdd.hAdd (α := ℤ) 0 1 - (↑{ val := y.g : InductionObj R y.n }.degBound : ℤ)) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
have this : { val := y.g : InductionObj R y.n }.degBound = 0
Tactic: have : degBound ⟨y.g⟩ = 0 := by nlinarith
-- 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
this : { val := y.g : InductionObj R y.n }.degBound = 0
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
have pos : { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤
  HPow.hPow (α := ℕ) (β := ℕ) 0 0
Tactic: rw [h, this]
-- 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
this : { val := y.g : InductionObj R y.n }.degBound = 0
pos :
  { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤
    HPow.hPow (α := ℕ) (β := ℕ) 0 0
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
have pos₁ : HPow.hPow (α := ℕ) (β := ℕ) 0 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 0
Tactic: rw [h, this]
-- 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
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound
have neg : 1 ≤ S.degBound
Tactic: gcongr