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
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
neg : (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound ^ c.degBound
⊢ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) ((c.val j).degree.succ * c'.degBound ^ c'.degBound) ≤
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.degBound ^ c.degBound)

Tactic:
apply pow_le_pow_right' c.one_le_coeffSubmodule

Premises used: _private.0.ChevalleyThm.PolynomialC.InductionObj.one_le_coeffSubmodule, pow_le_pow_right'
-- 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
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
dsimp :
  LT.lt (α := ℕ)
    (∑ i_1 : Fin n, (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) i_1).degree.succ)
    (∑ i : Fin n, (c.val i).degree.succ)
⊢ c'.degBound < c.degBound

Tactic:
dsimp [InductionObj.degBound, c']

Premises used: _private.0.ChevalleyThm.PolynomialC.InductionObj.degBound
-- 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
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
apply :
  ∀ (i_1 : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ i_1 →
      (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) i_1).degree.succ ≤
        (c.val i_1).degree.succ
apply₁ :
  (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) j).degree.succ < (c.val j).degree.succ
⊢ LT.lt (α := ℕ)
    (∑ i_1 : Fin n, (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) i_1).degree.succ)
    (∑ i : Fin n, (c.val i).degree.succ)

Tactic:
apply Finset.sum_lt_sum ?_ ⟨j, Finset.mem_univ _, ?_⟩

Premises used: Finset.mem_univ, And.intro, Exists.intro, Finset.sum_lt_sum
-- 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_1 : Fin C.n
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
_ :
  Membership.mem (γ := Finset (Fin n)) Finset.univ k →
    (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) k).degree.succ ≤ (c.val k).degree.succ
⊢ Membership.mem (γ := Finset (Fin n)) Finset.univ k →
    (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) k).degree.succ ≤ (c.val k).degree.succ

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 : 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_1 : Fin C.n
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ k
rw : (if k = j then c.val j %ₘ c.val i else c.val k).degree.succ ≤ (c.val k).degree.succ
⊢ (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) k).degree.succ ≤ (c.val k).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_1 : Fin C.n
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ k
pos : ∀ (hkj : k = j), (c.val j %ₘ c.val i).degree.succ ≤ (c.val k).degree.succ
neg : ∀ (hkj : ¬k = j), (c.val k).degree.succ ≤ (c.val k).degree.succ
⊢ (if k = j then c.val j %ₘ c.val i else c.val k).degree.succ ≤ (c.val k).degree.succ

Tactic:
split_ifs with hkj
-- 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 : Fin n
hi : (c.val i).Monic
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
C : BasicConstructibleSetData R
hC : C ∈ S
k_1 : Fin C.n
hi' : ¬c.val i = 1
k : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ k
hle : (c.val i).degree ≤ (c.val k).degree
hne : i ≠ k
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 k (c.val k %ₘ c.val i) : InductionObj R n }
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ 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 k (c.val k %ₘ 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 k (c.val k %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ c.val i) :
                InductionObj R n }.powBound
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val k).degree.succ
pos : (c.val k %ₘ c.val i).degree ≤ (c.val k).degree
⊢ (c.val k %ₘ c.val i).degree.succ ≤ (c.val k).degree.succ

Tactic:
gcongr
-- 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 : Fin n
hi : (c.val i).Monic
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
C : BasicConstructibleSetData R
hC : C ∈ S
k_1 : Fin C.n
hi' : ¬c.val i = 1
k : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ k
hle : (c.val i).degree ≤ (c.val k).degree
hne : i ≠ k
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 k (c.val k %ₘ c.val i) : InductionObj R n }
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ 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 k (c.val k %ₘ 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 k (c.val k %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ c.val i) :
                InductionObj R n }.powBound
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val k).degree.succ
⊢ (c.val k %ₘ c.val i).degree ≤ (c.val k).degree

Tactic:
(degree_modByMonic_le _ hi).trans hle

Premises used: Polynomial.degree_modByMonic_le, LE.le.trans
-- 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 : Fin n
hi : (c.val i).Monic
R₀ : Type u_1
inst_2 : CommRing R₀
inst_3 : Algebra R₀ R
f : R[X]
h : Nontrivial R
S : ConstructibleSetData R
C : BasicConstructibleSetData R
hC : C ∈ S
k_1 : Fin C.n
hi' : ¬c.val i = 1
k : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ k
hle : (c.val i).degree ≤ (c.val k).degree
hne : i ≠ k
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 k (c.val k %ₘ c.val i) : InductionObj R n }
hS :
  comap Polynomial.C ''
      (zeroLocus
          (Set.range
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ 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 k (c.val k %ₘ 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 k (c.val k %ₘ c.val i) : InductionObj R n })
            { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ c.val i) :
                InductionObj R n }.powBound
c' : InductionObj R n := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val k).degree.succ
⊢ (c.val k %ₘ c.val i).degree ≤ (c.val k).degree

Tactic:
exact (degree_modByMonic_le _ hi).trans hle

Premises used: Polynomial.degree_modByMonic_le, LE.le.trans
-- 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_1 : Fin C.n
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
k : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) Finset.univ k
hkj : ¬k = j
⊢ (c.val k).degree.succ ≤ (c.val k).degree.succ

Tactic:
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
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
hxy : (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) j).degree < (c.val j).degree
⊢ (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) j).degree.succ < (c.val j).degree.succ

Tactic:
gcongr
-- 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
hij : coeffSubmodule R₀ c' ≤ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
hi' : ¬c.val i = 1
⊢ (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) j).degree < (c.val j).degree

Tactic:
simpa using (degree_modByMonic_lt _ hi).trans_le hle

Premises used: LT.lt.trans_le, Polynomial.degree_modByMonic_lt