Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: case hP₃.inr.refine_2
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : 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_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
⊢ coeffSubmodule R₀ c' ^ c'.degBound ^ c'.degBound ≤ coeffSubmodule R₀ c ^ c.degBound ^ c.degBound

Tactic:
suffices hij : c'.coeffSubmodule R₀ ≤ c.coeffSubmodule R₀ ^ (c.val j).degree.succ by
        by_cases hi' : c.val i = 1
        · gcongr
          · exact c.one_le_coeffSubmodule
          · refine Submodule.span_le.mpr (Set.union_subset ?_ ?_)
            · exact Set.subset_union_left.trans Submodule.subset_span
            · refine Set.iUnion_subset fun k ↦ ?_
              simp only [update_apply, hi', modByMonic_one, c']
              split_ifs
              · rintro _ ⟨_, rfl⟩
                exact zero_mem _
              · exact (Set.subset_iUnion (fun i ↦ coeff(c.val i)) k).trans
                  (Set.subset_union_right.trans Submodule.subset_span)
          rw [Nat.one_le_iff_ne_zero, ← Nat.pos_iff_ne_zero, InductionObj.degBound]
          refine Fintype.sum_pos (Pi.lt_def.mpr ⟨by positivity, i, by simp [hi']⟩)
        refine (pow_le_pow_left' hij _).trans ?_
        rw [← pow_mul]
        apply pow_le_pow_right' c.one_le_coeffSubmodule
        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
        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

Goal state after:
case hP₃.inr.refine_2
R✝ : Type u_2
inst✝³ : CommRing R✝
n : ℕ
R : Type u_2
inst✝² : 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_1 : Algebra R₀ R],
    Statement R₀ R n { val := Function.update c.val j (c.val j %ₘ c.val i) }
R₀ : Type u_1
inst✝¹ : CommRing R₀
inst✝ : Algebra R₀ R
f : R[X]
h✝ : Nontrivial R
S : ConstructibleSetData R
hS :
  comap Polynomial.C ''
      (zeroLocus (Set.range { val := Function.update c.val j (c.val j %ₘ c.val i) }.val) \ zeroLocus {f}) =
    S.toSet
hS' :
  ∀ C ∈ S,
    C.n ≤ { val := Function.update c.val j (c.val j %ₘ c.val i) }.degBound ∧
      ∀ (i_1 : Fin C.n),
        C.g i_1 ∈
          coeffSubmodule R₀ { val := Function.update c.val j (c.val j %ₘ c.val i) } ^
            { val := Function.update c.val j (c.val j %ₘ c.val i) }.powBound
C : BasicConstructibleSetData R
hC : C ∈ S
c' : InductionObj R n := { val := Function.update c.val j (c.val j %ₘ c.val i) }
deg_bound₁ : c'.degBound ≤ c.degBound
k : Fin C.n
⊢ coeffSubmodule R₀ c' ≤ coeffSubmodule R₀ c ^ (c.val j).degree.succ