-- 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_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 j %ₘ c.val i).degree.succ ≤ (c.val k).degree.succ
have pos : ∀ (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),
  let c' := { val := Function.update (β := fun (a : Fin n) ↦ R[X]) c.val k (c.val k %ₘ c.val i) : InductionObj R n };
  ∀ (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.succ ≤ (c.val k).degree.succ
Tactic: subst hkj
Cleared hypotheses: j, hle, hne, H, hS, hS', c', deg_bound₁, hij, hkj