awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
refine : ⊥ < (c.val i).degree
⊢ ⊥ < (c.val j).degree

Tactic:
refine lt_of_lt_of_le ?_ hle

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
rw : ¬c.val i = 0
⊢ ⊥ < (c.val i).degree

Tactic:
rw [bot_lt_iff_ne_bot, ne_eq, degree_eq_bot]

Premises used: bot_lt_iff_ne_bot, ne_eq, Polynomial.degree_eq_bot
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
e : c.val i = 0
⊢ False

Tactic:
simp [e] at hi
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
⊢ (c.val j).degree.succ ≠ 0

Tactic:
have : (c.val j).degree.succ ≠ 0 := by
            rw [← Nat.pos_iff_ne_zero]
            apply WithBot.succ_lt_succ (x := ⊥)
            refine lt_of_lt_of_le ?_ hle
            rw [bot_lt_iff_ne_bot, ne_eq, degree_eq_bot]
            intro e
            simp [e] at hi
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
this : (c.val j).degree.succ ≠ 0
⊢ (c.val l).coeff m ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ

Tactic:
le_self_pow c.one_le_coeffSubmodule this ?_

Premises used: Set.Mem, _private.0.ChevalleyThm.PolynomialC.InductionObj.one_le_coeffSubmodule, le_self_pow
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
this : (c.val j).degree.succ ≠ 0
neg : Membership.mem (γ := Submodule R₀ R) (coeffSubmodule R₀ c) ((c.val l).coeff m)
⊢ (c.val l).coeff m ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ

Tactic:
refine le_self_pow c.one_le_coeffSubmodule this ?_

Premises used: _private.0.ChevalleyThm.PolynomialC.InductionObj.one_le_coeffSubmodule, le_self_pow
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
this : (c.val j).degree.succ ≠ 0
⊢ Membership.mem (γ := Submodule R₀ R) (coeffSubmodule R₀ c) ((c.val l).coeff m)

Tactic:
Submodule.subset_span (.inr (Set.mem_iUnion_of_mem l ⟨m, rfl⟩))

Premises used: Set.Mem, Set.mem_iUnion_of_mem, Exists.intro, Submodule.subset_span, Or.inr, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : InductionObj R n
i j : Fin n
hi : (c.val i).Monic
hle : (c.val i).degree ≤ (c.val j).degree
hne : i ≠ j
H :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra R₀ R],
    Statement R₀ R n
      { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.val) \
        zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤
        { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
            InductionObj R n }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          HPow.hPow (α := Submodule R₀ R)
            (coeffSubmodule R₀
              { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) :
                InductionObj R n }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
l : Fin n
m : ℕ
hlj : ¬l = j
this : (c.val j).degree.succ ≠ 0
⊢ Membership.mem (γ := Submodule R₀ R) (coeffSubmodule R₀ c) ((c.val l).coeff m)

Tactic:
exact Submodule.subset_span (.inr (Set.mem_iUnion_of_mem l ⟨m, rfl⟩))

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
hP₄ :
  ∀ [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra.{u_1, u_2} R₀ (Away c)],
            Statement R₀ (Away c) n
              {
                val :=
                  HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                    ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                    ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
                InductionObj (Away c) n }) →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀]
              [inst_2 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
              Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
                {
                  val :=
                    (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                        (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                      e.val }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
⊢ ∀ [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra.{u_1, u_2} R₀ (Away c)],
            Statement R₀ (Away c) n
              {
                val :=
                  HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                    ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                    ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
                InductionObj (Away c) n }) →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀]
              [inst_2 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
              Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
                {
                  val :=
                    (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                        (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                      e.val }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_2 : Algebra.{u_1, u_2} R₀ (Away c)],
    Statement R₀ (Away c) n
      {
        val :=
          HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
            ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
            ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
        InductionObj (Away c) n }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀]
    [inst_2 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
    Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
      {
        val :=
          (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
              (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
            e.val }
R₀ : Type u_1
hP₄ : ∀ [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
⊢ ∀ [inst : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_3 : Algebra.{u_1, u_2} R₀ (Away c)],
    Statement R₀ (Away c) n
      {
        val :=
          HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
            ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
            ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
        InductionObj (Away c) n }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀]
    [inst_3 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
    Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
      {
        val :=
          (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
              (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
            e.val }
R₀ : Type u_1
inst_2 : CommRing R₀
hP₄ : ∀ [inst : Algebra R₀ R], Statement R₀ R n e
⊢ ∀ [inst : Algebra R₀ R], Statement R₀ R n e

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra.{u_1, u_2} R₀ (Away c)],
    Statement R₀ (Away c) n
      {
        val :=
          HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
            ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
            ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
        InductionObj (Away c) n }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀]
    [inst_4 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
    Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
      {
        val :=
          (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
              (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
            e.val }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
⊢ Statement R₀ R n e

Tactic:
induction_aux (R₀ := R₀) R c i e he hc H₁ H₂

Premises used: _private.0.ChevalleyThm.PolynomialC.induction_aux
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R_1 : Type u_2
inst : CommRing R_1
n : ℕ
R : Type u_2
inst_1 : CommRing R
c : R
i : Fin n
e : InductionObj R n
he : c = (e.val i).leadingCoeff
hc : c ≠ 0
H₁ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀] [inst_4 : Algebra.{u_1, u_2} R₀ (Away c)],
    Statement R₀ (Away c) n
      {
        val :=
          HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
            ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
            ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
        InductionObj (Away c) n }
H₂ :
  ∀ {R₀ : Type u_1} [inst : CommRing R₀]
    [inst_4 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
    Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
      {
        val :=
          (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
              (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
            e.val }
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
⊢ Statement R₀ R n e

Tactic:
exact induction_aux (R₀ := R₀) R c i e he hc H₁ H₂

Premises used: _private.0.ChevalleyThm.PolynomialC.induction_aux
-- 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
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

Tactic:
choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f

Premises used: _private.0.ChevalleyThm.PolynomialC.statement, PrimeSpectrum.BasicConstructibleSetData.f, PrimeSpectrum.BasicConstructibleSetData.g, _private.0.ChevalleyThm.PolynomialC.InductionObj.mk