-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_2
inst : CommRing R
n : ℕ
hP₁ :
  ∀ (R : Type u_2) [inst : CommRing R] {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
    Statement R₀ R n { val := 0 }
hP₂ :
  ∀ (R : Type u_2) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₃ :
  ∀ (R : Type u_2) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
              Statement R₀ R n
                { val := Function.update (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) :
                  InductionObj R n }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₄ :
  ∀ (R : Type u_2) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra.{u_1, u_2} R₀ (Away c)],
            Statement R₀ (Away c) n
              {
                val :=
                  HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                    ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                    ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
                InductionObj (Away c) n }) →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀]
              [inst_2 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
              Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
                {
                  val :=
                    (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                        (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                      e.val }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₅ :
  ∀ (R : Type u_2) [inst : CommRing R] (e : InductionObj R n) (i : Fin n),
    (e.val i).Monic →
      (∀ (j : Fin n), j ≠ i → e.val j = 0) →
        ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₆ :
  ∀ (R : Type u_2) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
              Statement R₀ R n
                { val := Function.update (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) :
                  InductionObj R n }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₇ :
  ∀ (R : Type u_2) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra.{u_1, u_2} R₀ (Away c)],
            Statement R₀ (Away c) n
              {
                val :=
                  HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                    ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                    ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
                InductionObj (Away c) n }) →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀]
              [inst_2 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
              Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
                {
                  val :=
                    (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                        (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                      e.val }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₈ :
  ∀ (R : Type u_2) [inst : CommRing R] (e : InductionObj R n) (i j : Fin n),
    (e.val i).Monic →
      (e.val i).degree ≤ (e.val j).degree →
        i ≠ j →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R],
              Statement R₀ R n
                { val := Function.update (β := fun (a : Fin n) ↦ R[X]) e.val j (e.val j %ₘ e.val i) :
                  InductionObj R n }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
hP₉ hP₁₀ :
  ∀ (R : Type u_2) [inst : CommRing R] (c : R) (i : Fin n) (e : InductionObj R n),
    c = (e.val i).leadingCoeff →
      c ≠ 0 →
        (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra.{u_1, u_2} R₀ (Away c)],
            Statement R₀ (Away c) n
              {
                val :=
                  HSMul.hSMul (α := (Away c)[X]) (β := Fin n → (Away c)[X])
                    ((Polynomial.C : (a : Away c) → (Away c)[X]) (IsLocalization.Away.invSelf c))
                    ((⇑(mapRingHom (algebraMap R (Away c))) : (a : R[X]) → (Away c)[X]) ∘ e.val) :
                InductionObj (Away c) n }) →
          (∀ {R₀ : Type u_1} [inst_1 : CommRing R₀]
              [inst_2 : Algebra.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))],
              Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n
                {
                  val :=
                    (⇑(mapRingHom (algebraMap R (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))) :
                        (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘
                      e.val }) →
            ∀ {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n e
⊢ ∀ (S : InductionObj R n) {R₀ : Type u_1} [inst_1 : CommRing R₀] [inst_2 : Algebra R₀ R], Statement R₀ R n S

Tactic:
classical
  apply induction_structure
  · intro R _ R₀ _ _ f
    refine ⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨f.coeff j, 0, 0⟩, ?_, ?_⟩
    · convert! image_comap_C_basicOpen f
      · simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_diff]
        congr 1
        rw [← Set.univ_subset_iff]
        rintro x _ _ ⟨_, rfl⟩
        exact zero_mem x.asIdeal
      · suffices Set.range f.coeff = ⋃ i < f.natDegree + 2, {f.coeff i} by
          simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet,
            ← Set.compl_eq_univ_diff, eq_compl_comm (y := zeroLocus _), ← zeroLocus_iUnion₂, this]
        trans f.coeff '' (Set.Iio (f.natDegree + 2))
        · refine ((Set.image_subset_range _ _).antisymm ?_).symm
          rintro _ ⟨i, rfl⟩
          by_cases! hi : i ≤ f.natDegree
          · exact ⟨i, hi.trans_lt (by simp), rfl⟩
          · exact ⟨f.natDegree + 1, by simp, by simp [f.coeff_eq_zero_of_natDegree_lt hi]⟩
        · ext; simp [eq_comm]
    · simp
  · intro R _ g i hi hi_min _ R₀ _ f
    let M := R[X] ⧸ Ideal.span {g.1 i}
    have : Module.Free R M := .of_basis (AdjoinRoot.powerBasis' hi).basis
    have : Module.Finite R M := .of_basis (AdjoinRoot.powerBasis' hi).basis
    refine ⟨(Finset.range (Module.finrank R M)).image
      fun j ↦ ⟨(Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0, 0⟩, ?_, ?_⟩
    · ext x
      have : zeroLocus (Set.range g.val) = zeroLocus {g.1 i} := by
        rw [Set.range_eq_iUnion, zeroLocus_iUnion]
        refine (Set.iInter_subset _ _).antisymm (Set.subset_iInter fun j ↦ ?_)
        by_cases hij : i = j
        · subst hij; rfl
        · rw [hi_min j (.symm hij), zeroLocus_singleton_zero]; exact Set.subset_univ _
      rw [this, ← Polynomial.algebraMap_eq, mem_image_comap_zeroLocus_sdiff,
        IsScalarTower.algebraMap_apply R[X] M, isNilpotent_tensor_residueField_iff]
      simp [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.subset_def, M]
    · simp
  · intro R _ c i j hi hle hne H R₀ _ _ f
    cases subsingleton_or_nontrivial R
    · use ∅
      simp [ConstructibleSetData.toSet, Subsingleton.elim f 0]
    obtain ⟨S, hS, hS'⟩ := H (R₀ := R₀) f
    refine ⟨S, Eq.trans ?_ hS, ?_⟩
    · rw [← zeroLocus_span (Set.range _), ← zeroLocus_span (Set.range _),
        idealSpan_range_update_divByMonic hne]
    · intro C hC
      let c' : InductionObj _ _ := ⟨update c.val j (c.val j %ₘ c.val i)⟩
      have deg_bound₁ : c'.degBound ≤ c.degBound := by
        dsimp [InductionObj.degBound, c']
        gcongr with k
        · rw [update_apply]
          split_ifs with hkj
          · subst hkj; exact (degree_modByMonic_le _ hi).trans hle
          · rfl
      refine ⟨(hS' C hC).1.trans deg_bound₁, fun k ↦ SetLike.le_def.mp ?_ ((hS' C hC).2 k)⟩
      change c'.coeffSubmodule R₀ ^ c'.powBound ≤ _
      delta powBound
      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
      rw [coeffSubmodule]
      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']
      constructor
      · apply one_le_pow_of_one_le' c.one_le_coeffSubmodule
        rw [Submodule.one_eq_span]
        exact Submodule.subset_span rfl
      · intro l m
        rw [update_apply]
        split_ifs with hlj
        · convert!
          coeff_modByMonic_mem_pow_natDegree_mul _ _ _ (fun _ ↦ coeff_mem_coeffSubmodule)
            one_mem_coeffSubmodule _ (fun _ ↦ coeff_mem_coeffSubmodule) one_mem_coeffSubmodule _
          rw [← pow_succ, Polynomial.degree_eq_natDegree, WithBot.succ_natCast, Nat.cast_id]
          intro e
          simp [show c.val i = 0 by simpa [e] using hle] at hi
        · have : (c.val j).degree.succ ≠ 0 := by
            rw [← Nat.pos_iff_ne_zero]
            apply WithBot.succ_lt_succ (x := ⊥)
            refine lt_of_lt_of_le ?_ hle
            rw [bot_lt_iff_ne_bot, ne_eq, degree_eq_bot]
            intro e
            simp [e] at hi
          refine le_self_pow c.one_le_coeffSubmodule this ?_
          exact Submodule.subset_span (.inr (Set.mem_iUnion_of_mem l ⟨m, rfl⟩))
  · intro R _ c i e he hc H₁ H₂ R₀ _ _
    exact induction_aux (R₀ := R₀) R c i e he hc H₁ H₂

Premises used: Set.univ_subset_iff, Set.singleton_subset_iff, PrimeSpectrum.BasicConstructibleSetData.toSet, Polynomial.degree_eq_natDegree, Nat.cast_id, Set.subset_def, Set.iUnion_subset_iff, Set.union_subset_iff, pow_succ, PrimeSpectrum.zeroLocus_span, Set.image_subset_range, Polynomial.coeff_modByMonic_mem_pow_natDegree_mul, subsingleton_or_nontrivial, Function.update_apply, eq_comm, _private.0.ChevalleyThm.PolynomialC.InductionObj.powBound, _private.0.ChevalleyThm.PolynomialC.InductionObj.coeff_mem_coeffSubmodule, isNilpotent_tensor_residueField_iff, SetLike.mem_coe, HasSubset.Subset.antisymm, _private.0.ChevalleyThm.PolynomialC.InductionObj.one_mem_coeffSubmodule, WithBot.succ_natCast, Set.compl_eq_univ_diff, _private.0.ChevalleyThm.PolynomialC.induction_structure, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Submodule.subset_span, Set.range, Set.range_subset_iff, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, Eq.symm, PrimeSpectrum.ConstructibleSetData.toSet, _private.0.ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule, Submodule.span_le, rfl, Polynomial.algebraMap_eq, Submodule.one_eq_span