-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R : Type u_6
inst : CommRing R
M : Submodule ℤ R
hM : 1 ∈ M
S : ConstructibleSetData R[X]
hS : ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), (C.g j).coeff k ∈ M
choose :
  ∀ (f : (C : BasicConstructibleSetData R[X]) → ConstructibleSetData R)
    (hf₁ :
      ∀ (C : BasicConstructibleSetData R[X]),
        comap Polynomial.C '' (zeroLocus (Set.range { val := C.g : InductionObj R C.n }.val) \ zeroLocus {C.f}) =
          (f C).toSet)
    (hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g : InductionObj R C.n }.degBound)
    (hf₃ :
      ∀ (C : BasicConstructibleSetData R[X]),
        ∀ C_1 ∈ f C,
          ∀ (i : Fin C_1.n),
            C_1.g i ∈
              HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := C.g : InductionObj R C.n })
                { val := C.g : InductionObj R C.n }.powBound),
    ∃ (T : ConstructibleSetData R),
      comap Polynomial.C '' S.toSet = T.toSet ∧
        ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
refine_1 :
  ∀ (f : (C : BasicConstructibleSetData R[X]) → ConstructibleSetData R)
    (hf₁ :
      ∀ (C : BasicConstructibleSetData R[X]),
        comap Polynomial.C '' (zeroLocus (Set.range { val := C.g : InductionObj R C.n }.val) \ zeroLocus {C.f}) =
          (f C).toSet)
    (hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g : InductionObj R C.n }.degBound)
    (hf₃ :
      ∀ (C : BasicConstructibleSetData R[X]),
        ∀ C_1 ∈ f C,
          ∀ (i : Fin C_1.n),
            C_1.g i ∈
              HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := C.g : InductionObj R C.n })
                { val := C.g : InductionObj R C.n }.powBound),
    comap Polynomial.C '' S.toSet = ConstructibleSetData.toSet (Finset.biUnion S f)
refine_2 refine_2₁ :
  ∀ (f : (C : BasicConstructibleSetData R[X]) → ConstructibleSetData R)
    (hf₁ :
      ∀ (C : BasicConstructibleSetData R[X]),
        comap Polynomial.C '' (zeroLocus (Set.range { val := C.g : InductionObj R C.n }.val) \ zeroLocus {C.f}) =
          (f C).toSet)
    (hf₂ : ∀ (C : BasicConstructibleSetData R[X]), ∀ C_1 ∈ f C, C_1.n ≤ { val := C.g : InductionObj R C.n }.degBound)
    (hf₃ :
      ∀ (C : BasicConstructibleSetData R[X]),
        ∀ C_1 ∈ f C,
          ∀ (i : Fin C_1.n),
            C_1.g i ∈
              HPow.hPow (α := Submodule ℤ R) (coeffSubmodule ℤ { val := C.g : InductionObj R C.n })
                { val := C.g : InductionObj R C.n }.powBound),
    ∀ C ∈ Finset.biUnion S f, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' S.toSet = T.toSet ∧
      ∀ C ∈ T, C.n ≤ S.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ M ^ S.degBound ^ S.degBound

Tactic:
classical
  choose f hf₁ hf₂ hf₃ using fun C : BasicConstructibleSetData R[X] ↦ statement (R₀ := ℤ) ⟨C.g⟩ C.f
  refine ⟨S.biUnion f, ?_, ?_⟩
  · simp only [BasicConstructibleSetData.toSet, ConstructibleSetData.toSet, Set.image_iUnion,
      Finset.set_biUnion_biUnion, hf₁]
  · simp only [Finset.mem_biUnion, forall_exists_index, and_imp]
    intro x y hy hx
    have H : degBound ⟨y.g⟩ ≤ S.degBound :=
      Finset.le_sup (f := fun e ↦ ∑ i, (e.g i).degree.succ) hy
    refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩
    gcongr
    · simpa [Submodule.one_eq_span]
    · refine Submodule.span_le.mpr ?_
      simp [Set.subset_def, hM, forall_comm (α := R), hS y hy]
    · delta powBound
      by_cases h : S.degBound = 0
      · have : degBound ⟨y.g⟩ = 0 := by nlinarith
        rw [h, this]
      gcongr
      rwa [Nat.one_le_iff_ne_zero]

Premises used: _private.0.ChevalleyThm.PolynomialC.statement, Iff.mpr, Finset.set_biUnion_biUnion, PrimeSpectrum.BasicConstructibleSetData.toSet, Set.subset_def, and_imp, forall_comm, forall_exists_index, PrimeSpectrum.BasicConstructibleSetData.f, PrimeSpectrum.ConstructibleSetData.degBound, PrimeSpectrum.BasicConstructibleSetData.g, _private.0.ChevalleyThm.PolynomialC.InductionObj.powBound, Set.image_iUnion, _private.0.ChevalleyThm.PolynomialC.InductionObj.mk, Nat.one_le_iff_ne_zero, PrimeSpectrum.ConstructibleSetData.toSet, Finset.mem_biUnion, Submodule.span_le, Submodule.one_eq_span