-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
inst : CommRing R₀
n : ℕ
R : Type u_6
inst_1 : CommRing R
inst_2 : Algebra R₀ R
c : R
i : Fin n
e : InductionObj R n
hi : c = (e.val i).leadingCoeff
hc : c ≠ 0
q₁ : R →ₐ[R₀] Localization.Away c := IsScalarTower.toAlgHom R₀ R (Localization.Away c)
q₂ : R →ₐ[R₀] HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}) := Ideal.Quotient.mkₐ R₀ (Ideal.span {c})
q₂_surjective :
  Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) (⇑q₂ : (a : R) → R ⧸ Ideal.span {c})
e₁ : InductionObj (Localization.Away c) n :=
  {
    val :=
      HSMul.hSMul (α := (Localization.Away c)[X]) (β := Fin n → (Localization.Away c)[X])
        ((Polynomial.C : (a : Localization.Away c) → (Localization.Away c)[X]) (IsLocalization.Away.invSelf c))
        ((⇑(mapRingHom (↑q₁ : R →+* Localization.Away c)) : (a : R[X]) → (Localization.Away c)[X]) ∘ e.val) }
e₂ : InductionObj (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n :=
  { val := (⇑(mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c})) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) ∘ e.val }
degBound_e₁_le : e₁.degBound ≤ e.degBound
degBound_e₂_lt : e₂.degBound < e.degBound
H₁ : Statement R₀ (Localization.Away c) n e₁
H₂ : Statement R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) n e₂
f : R[X]
T₁ : ConstructibleSetData (Localization.Away c)
T₂ : ConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
hT₁ :
  comap Polynomial.C ''
      (zeroLocus (Set.range e₁.val) \
        zeroLocus
          (singleton (α := (Localization.Away c)[X])
            ((mapRingHom (↑q₁ : R →+* Localization.Away c) : (a : R[X]) → (Localization.Away c)[X]) f :
              (Localization.Away c)[X]))) =
    T₁.toSet
hT₁deg : ∀ (x : BasicConstructibleSetData (Localization.Away c)) (x_1 : x ∈ T₁), x.n ≤ e₁.degBound
hT₂ :
  comap Polynomial.C ''
      (zeroLocus (Set.range e₂.val) \
        zeroLocus
          (singleton (α := (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X])
            ((mapRingHom (↑q₂ : R →+* R ⧸ Ideal.span {c}) : (a : R[X]) → (R ⧸ Ideal.span {c})[X]) f :
              (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))[X]))) =
    T₂.toSet
hT₂deg :
  ∀ (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (x_1 : x ∈ T₂),
    x.n ≤ e₂.degBound
x : Invertible (α := Localization.Away c) ((q₁ : (a : R) → Localization.Away c) c) :=
  { invOf := IsLocalization.Away.invSelf c, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
he₁span :
  HPow.hPow (α := Submodule R₀ (Localization.Away c)) (coeffSubmodule R₀ e₁) e₁.powBound =
    @Invertible.invOf _ MulOne.toMul MulOne.toOne
        (HPow.hPow (α := Localization.Away c) ((q₁ : (a : R) → Localization.Away c) c) e₁.powBound) _ •
      Submodule.map q₁.toLinearMap
        (HPow.hPow (α := Submodule R₀ R) (span R₀ ({c} ∪ ⋃ (i : Fin n), coeff(e.val i))) e₁.powBound)
g₁ : (x : BasicConstructibleSetData (Localization.Away c)) → (i : Fin x.n) → R
hg₁ :
  ∀ (x : BasicConstructibleSetData (Localization.Away c)) (hx : x ∈ T₁) (i : Fin x.n),
    g₁ x i ∈ (↑(HPow.hPow (α := Submodule R₀ R) (span R₀ ({c} ∪ ⋃ (i : Fin n), coeff(e.val i))) e₁.powBound) : Set R)
hq₁g₁ :
  ∀ (x : BasicConstructibleSetData (Localization.Away c)) (hx : x ∈ T₁) (i : Fin x.n),
    (q₁.toLinearMap : (a : R) → Localization.Away c) (g₁ x i) =
      HPow.hPow (α := Localization.Away c) ((q₁ : (a : R) → Localization.Away c) c) e₁.powBound * x.g i
n₁ : (z : Localization.Away c) → ℕ
f₁ : (z : Localization.Away c) → R
hf₁ :
  ∀ (x : Localization.Away c),
    x * HPow.hPow (α := Localization.Away c) ((q₁ : (a : R) → Localization.Away c) c) (n₁ x) =
      (q₁ : (a : R) → Localization.Away c) (f₁ x)
g₂ : (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) → (i : Fin x.n) → R
hg₂ :
  ∀ (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (x_1 : x ∈ T₂)
    (i : Fin x.n), g₂ x i ∈ (↑(HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e₂.powBound) : Set R)
hq₂g₂ :
  ∀ (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (x_1 : x ∈ T₂)
    (i : Fin x.n), (q₂.toLinearMap : (a : R) → R ⧸ Ideal.span {c}) (g₂ x i) = x.g i
f₂ : (b : HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})) → R
hf₂ : ∀ (x : HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})), (q₂ : (a : R) → R ⧸ Ideal.span {c}) (f₂ x) = x
S₁ : Finset (BasicConstructibleSetData R) :=
  Finset.image (fun (x : BasicConstructibleSetData (Localization.Away c)) ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x }) T₁
S₂ : Finset (BasicConstructibleSetData R) :=
  Finset.image
    (fun (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) ↦
      { f := f₂ x.f, n := x.n + 1, g := Fin.cons (α := fun (a : Fin (x.n + 1)) ↦ R) c (g₂ x) })
    T₂
refine_2 :
  ∀ (x : BasicConstructibleSetData (Localization.Away c)) (hx : x ∈ T₁) (k : Fin x.n),
    (↑(HPow.hPow (α := Submodule R₀ R) (span R₀ ({c} ∪ ⋃ (i : Fin n), coeff(e.val i))) e₁.powBound) : Set R) ⊆
      (↑(HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound) : Set R)
refine_2₁ :
  ∀ (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (hx : x ∈ T₂),
    Membership.mem (α := R) (HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound)
      (Fin.cons (α := fun (a : Fin (x.n + 1)) ↦ R) c (g₂ x) 0 : R)
refine_2₂ :
  ∀ (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (hx : x ∈ T₂)
    (k : Fin x.n),
    (↑(HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e₂.powBound) : Set R) ⊆
      (↑(HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound) : Set R)
⊢ ((∀ ⦃x : BasicConstructibleSetData (Localization.Away c)⦄, x ∈ T₁ → x.n ≤ e.degBound) ∧
      ∀ ⦃x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))⦄,
        x ∈ T₂ → x.n + 1 ≤ e.degBound) ∧
    (∀ ⦃x : BasicConstructibleSetData (Localization.Away c)⦄,
        x ∈ T₁ → ∀ (i : Fin x.n), g₁ x i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound) ∧
      ∀ ⦃x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))⦄,
        x ∈ T₂ →
          ∀ (i : Fin (x.n + 1)),
            Membership.mem (α := R) (HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound)
              (Fin.cons (α := fun (a : Fin (x.n + 1)) ↦ R) c (g₂ x) i : R)

Tactic:
refine ⟨⟨fun x hx ↦ (hT₁deg _ hx).trans degBound_e₁_le,
      fun x hx ↦ (hT₂deg _ hx).trans_lt degBound_e₂_lt⟩,
      fun x hx k ↦ SetLike.mem_of_subset ?_ (hg₁ _ hx _),
      fun x hx ↦ Fin.cons ?_ fun k ↦ SetLike.mem_of_subset ?_ (hg₂ _ hx _)⟩