awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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

Tactic:
⟨S.biUnion f, ?_, ?_⟩

Premises used: Finset.biUnion, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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)
refine_2 : ∀ C ∈ Finset.biUnion S f, 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

Tactic:
refine ⟨S.biUnion f, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
⊢ comap Polynomial.C '' S.toSet = ConstructibleSetData.toSet (Finset.biUnion S f)

Tactic:
simp only [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.image_iUnion,
      Finset.set_biUnion_biUnion, hf₁]

Premises used: Finset.set_biUnion_biUnion, PrimeSpectrum.BasicConstructibleSetData.toSet, Set.image_iUnion, PrimeSpectrum.ConstructibleSetData.toSet
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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_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
⊢ ∀ C ∈ Finset.biUnion S f, 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]

Premises used: and_imp, forall_exists_index, Finset.mem_biUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
⊢ { 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
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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

Tactic:
⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩

Premises used: SetLike.le_def, And.intro, Iff.mp, LE.le.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
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
⊢ x.n ≤ S.degBound ∧ ∀ (i : Fin x.n), x.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
refine_2₂ : { val := y.g : InductionObj R y.n }.powBound ≤ S.degBound ^ S.degBound
⊢ 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:
gcongr
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
⊢ 1 ≤ M

Tactic:
simpa [Submodule.one_eq_span]

Premises used: Submodule.one_eq_span
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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

Tactic:
Submodule.span_le.mpr ?_

Premises used: Iff.mpr, Set.Mem, Submodule.span_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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} ∪ ⋃ (i : Fin y.n), Set.range ({ val := y.g : InductionObj R y.n }.val i).coeff ⊆ (↑M : Set R)
⊢ coeffSubmodule ℤ { val := y.g : InductionObj R y.n } ≤ M

Tactic:
refine Submodule.span_le.mpr ?_

Premises used: Iff.mpr, Submodule.span_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
⊢ {1} ∪ ⋃ (i : Fin y.n), Set.range ({ val := y.g : InductionObj R y.n }.val i).coeff ⊆ (↑M : Set R)

Tactic:
simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]

Premises used: Set.subset_def, forall_comm
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
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
⊢ { 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

Premises used: PrimeSpectrum.ConstructibleSetData.degBound
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
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
⊢ { val := y.g : InductionObj R y.n }.degBound = 0

Tactic:
nlinarith
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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

Tactic:
have : degBound ⟨y.g⟩ = 0 := by nlinarith
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
pos₁ pos₂ : HPow.hPow (α := ℕ) (β := ℕ) 0 0 ≤ HPow.hPow (α := ℕ) (β := ℕ) 0 0
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound

Tactic:
rw [h, this]
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
neg : 1 ≤ S.degBound
⊢ { val := y.g : InductionObj R y.n }.degBound ^ { val := y.g : InductionObj R y.n }.degBound ≤ S.degBound ^ S.degBound

Tactic:
gcongr
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
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
neg neg₁ neg₂ neg₃ : S.degBound ≠ 0
⊢ 1 ≤ S.degBound

Tactic:
rwa [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k : ℕ
D : ℕ → ℕ
rw rw₁ : Eq (α := ℕ) 1 1
⊢ degBound k D 0 = 1

Tactic:
rw [degBound]

Premises used: ChevalleyThm.MvPolynomialC.degBound
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k : ℕ
D : ℕ → ℕ
rw rw₁ : k = k
⊢ numBound k D 0 = k

Tactic:
rw [numBound]

Premises used: ChevalleyThm.MvPolynomialC.numBound
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k : ℕ
D : ℕ → ℕ
n : ℕ
rw 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) = numBound k D (n + 1) ^ numBound k D (n + 1) * degBound k D n

Tactic:
rw [degBound]

Premises used: ChevalleyThm.MvPolynomialC.degBound
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
k : ℕ
D : ℕ → ℕ
n : ℕ
rw 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 * degBound k D n * D n

Tactic:
rw [numBound]

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

Tactic:
simp