-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity (hypothesis)
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)
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 ∧
    ∀ C ∈ T₁,
      C.n ≤ e₁.degBound ∧
        ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ (Localization.Away c)) (coeffSubmodule R₀ e₁) e₁.powBound
T₂ : ConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))
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 ∧
    ∀ C ∈ T₂,
      C.n ≤ e₂.degBound ∧
        ∀ (i : Fin C.n),
          C.g i ∈
            HPow.hPow (α := Submodule R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c})))
              (coeffSubmodule R₀ e₂) e₂.powBound
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 ∧
    (∀ (x : BasicConstructibleSetData (Localization.Away c)) (x_1 : x ∈ T₁), x.n ≤ e₁.degBound) ∧
      ∀ (x : BasicConstructibleSetData (Localization.Away c)) (x_1 : x ∈ T₁) (i : Fin x.n),
        x.g i ∈ HPow.hPow (α := Submodule R₀ (Localization.Away c)) (coeffSubmodule R₀ e₁) e₁.powBound
⊢ ∃ (T : ConstructibleSetData R),
    comap Polynomial.C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) = T.toSet ∧
      ∀ C ∈ T,
        C.n ≤ e.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (coeffSubmodule R₀ e) e.powBound
have 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 ∧
  (∀ (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (x_1 : x ∈ T₂),
      x.n ≤ e₂.degBound) ∧
    ∀ (x : BasicConstructibleSetData (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (x_1 : x ∈ T₂)
      (i : Fin x.n),
      x.g i ∈
        HPow.hPow (α := Submodule R₀ (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {c}))) (coeffSubmodule R₀ e₂)
          e₂.powBound
Tactic: simp only [forall_and] at hT₁ hT₂
Cleared hypotheses: hT₁, hT₂