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
hP₃ : Membership.mem (γ := Submodule R₀ R) (R₀ ∙ 1) 1
⊢ Membership.mem (γ := Submodule R₀ R) 1 1

Tactic:
rw [Submodule.one_eq_span]

Premises used: Submodule.one_eq_span
-- 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
⊢ Membership.mem (γ := Submodule R₀ R) (R₀ ∙ 1) 1

Tactic:
Submodule.subset_span rfl

Premises used: Set.Mem, Submodule.subset_span, 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
⊢ Membership.mem (γ := Submodule R₀ R) (R₀ ∙ 1) 1

Tactic:
exact Submodule.subset_span rfl

Premises used: Submodule.subset_span, 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 : ℕ
hP₃ :
  (if l = j then c.val j %ₘ c.val i else c.val l).coeff m ∈
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
⊢ (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) l).coeff m ∈
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ

Tactic:
rw [update_apply]

Premises used: Function.update_apply
-- 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 : ℕ
pos :
  ∀ (hlj : l = j),
    (c.val j %ₘ c.val i).coeff m ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
neg : ∀ (hlj : ¬l = j), (c.val l).coeff m ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
⊢ (if l = j then c.val j %ₘ c.val i else c.val l).coeff m ∈
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ

Tactic:
split_ifs with hlj
-- 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 %ₘ c.val i).coeff m ∈
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).natDegree * coeffSubmodule R₀ c

Tactic:
coeff_modByMonic_mem_pow_natDegree_mul _ _ _ (fun _ ↦ coeff_mem_coeffSubmodule)
            one_mem_coeffSubmodule _ (fun _ ↦ coeff_mem_coeffSubmodule) one_mem_coeffSubmodule _

Premises used: Polynomial.coeff_modByMonic_mem_pow_natDegree_mul, _private.0.ChevalleyThm.PolynomialC.InductionObj.coeff_mem_coeffSubmodule, _private.0.ChevalleyThm.PolynomialC.InductionObj.one_mem_coeffSubmodule
-- 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_1 : 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
h :
  HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ =
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).natDegree * coeffSubmodule R₀ c
⊢ (c.val j %ₘ c.val i).coeff m ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ

Tactic:
convert!
          coeff_modByMonic_mem_pow_natDegree_mul _ _ _ (fun _ ↦ coeff_mem_coeffSubmodule)
            one_mem_coeffSubmodule _ (fun _ ↦ coeff_mem_coeffSubmodule) one_mem_coeffSubmodule _

Premises used: Polynomial.coeff_modByMonic_mem_pow_natDegree_mul, _private.0.ChevalleyThm.PolynomialC.InductionObj.coeff_mem_coeffSubmodule, _private.0.ChevalleyThm.PolynomialC.InductionObj.one_mem_coeffSubmodule
-- 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_1 : 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
h : c.val j ≠ 0
⊢ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ =
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).natDegree * coeffSubmodule R₀ c

Tactic:
rw [← pow_succ, Polynomial.degree_eq_natDegree, WithBot.succ_natCast, Nat.cast_id]

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_id, pow_succ, WithBot.succ_natCast
-- 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 j = 0
⊢ c.val i = 0

Tactic:
simpa [e] using hle
-- 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 j = 0
⊢ False

Tactic:
simp [show c.val i = 0 by simpa [e] using hle] 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
rw : 0 < (c.val j).degree.succ
⊢ (c.val j).degree.succ ≠ 0

Tactic:
rw [← Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- 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
apply : ⊥ < (c.val j).degree
⊢ 0 < (c.val j).degree.succ

Tactic:
apply WithBot.succ_lt_succ (x := ⊥)

Premises used: WithBot.succ_lt_succ
-- 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

Tactic:
lt_of_lt_of_le ?_ hle

Premises used: lt_of_lt_of_le