awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound ^ c.degBound
have deg_bound₂ : c'.degBound < c.degBound
Tactic: have deg_bound₂ : c'.degBound < c.degBound := by
          dsimp [InductionObj.degBound, c']
          apply Finset.sum_lt_sum ?_ ⟨j, Finset.mem_univ _, ?_⟩
          · intro k _
            rw [update_apply]
            split_ifs with hkj
            · subst hkj; gcongr; exact (degree_modByMonic_le _ hi).trans hle
            · rfl
          · gcongr; simpa using (degree_modByMonic_lt _ hi).trans_le hle
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
deg_bound₂ : c'.degBound < c.degBound
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound * c.degBound ^ c'.degBound
have h₁ : (c.val j).degree.succ ≤ c.degBound
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
deg_bound₂ : c'.degBound < c.degBound
⊢ c.degBound * c.degBound ^ c'.degBound = c.degBound ^ (c'.degBound + 1)
have rw : c.degBound * c.degBound ^ c'.degBound = c.degBound * c.degBound ^ c'.degBound
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
deg_bound₂ : c'.degBound < c.degBound
⊢ c.degBound ^ (c'.degBound + 1) ≤ c.degBound ^ c.degBound
have ha : 1 ≤ c.degBound
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
deg_bound₂ : c'.degBound < c.degBound
ha : 1 ≤ c.degBound
⊢ c.degBound ^ (c'.degBound + 1) ≤ c.degBound ^ c.degBound
have hmn : c'.degBound + 1 ≤ c.degBound
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
deg_bound₂ : c'.degBound < c.degBound
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound ^ c.degBound
have calc : (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound * c.degBound ^ c'.degBound
Tactic: calc (c.val j).degree.succ * c'.degBound ^ c'.degBound
          _ ≤ c.degBound * c.degBound ^ c'.degBound := by
            gcongr
            delta InductionObj.degBound
            exact Finset.single_le_sum (f := fun i ↦ (c.val i).degree.succ)
              (by intros; positivity) (Finset.mem_univ _)
          _ = c.degBound ^ (c'.degBound + 1) := by rw [pow_succ']
          _ ≤ c.degBound ^ c.degBound := by gcongr <;> lia
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
deg_bound₂ : c'.degBound < c.degBound
calc : (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound * c.degBound ^ c'.degBound
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound ^ c.degBound
have calc₁ : c.degBound * c.degBound ^ c'.degBound = c.degBound ^ (c'.degBound + 1)
Tactic: calc (c.val j).degree.succ * c'.degBound ^ c'.degBound
          _ ≤ c.degBound * c.degBound ^ c'.degBound := by
            gcongr
            delta InductionObj.degBound
            exact Finset.single_le_sum (f := fun i ↦ (c.val i).degree.succ)
              (by intros; positivity) (Finset.mem_univ _)
          _ = c.degBound ^ (c'.degBound + 1) := by rw [pow_succ']
          _ ≤ c.degBound ^ c.degBound := by gcongr <;> lia
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
deg_bound₂ : c'.degBound < c.degBound
calc : (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound * c.degBound ^ c'.degBound
calc₁ : c.degBound * c.degBound ^ c'.degBound = c.degBound ^ (c'.degBound + 1)
⊢ (c.val j).degree.succ * c'.degBound ^ c'.degBound ≤ c.degBound ^ c.degBound
have calc₂ : c.degBound ^ (c'.degBound + 1) ≤ c.degBound ^ c.degBound
Tactic: calc (c.val j).degree.succ * c'.degBound ^ c'.degBound
          _ ≤ c.degBound * c.degBound ^ c'.degBound := by
            gcongr
            delta InductionObj.degBound
            exact Finset.single_le_sum (f := fun i ↦ (c.val i).degree.succ)
              (by intros; positivity) (Finset.mem_univ _)
          _ = c.degBound ^ (c'.degBound + 1) := by rw [pow_succ']
          _ ≤ c.degBound ^ c.degBound := by gcongr <;> lia
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ Submodule.span R₀ ({1} ∪ ⋃ (i : Fin n), coeff(c'.val i)) ≤
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
have hP₃ : 1 ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ ∧
  ∀ (i_1 : Fin n) (y : ℕ),
    (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) i_1).coeff y ∈
      HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
Tactic: simp only [Submodule.span_le, Set.union_subset_iff, Set.singleton_subset_iff, SetLike.mem_coe,
        Set.iUnion_subset_iff, Set.range_subset_iff, c']
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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
⊢ 1 ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ ∧
    ∀ (i_1 : Fin n) (y : ℕ),
      (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) i_1).coeff y ∈
        HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
have hP₃ : 1 ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (goal)
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₃ : 1 ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
⊢ 1 ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ ∧
    ∀ (i_1 : Fin n) (y : ℕ),
      (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) i_1).coeff y ∈
        HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
have hP₄ : ∀ (i_1 : Fin n) (y : ℕ),
  (Function.update (β := fun (a : Fin n) ↦ R[X]) c.val j (c.val j %ₘ c.val i) i_1).coeff y ∈
    HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ c) (c.val j).degree.succ
Tactic: constructor