-- 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
let let₁ let₂ let₃ :
  ∃ (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
refine_1 :
  let S₁ : Finset (BasicConstructibleSetData R) :=
    Finset.image (fun (x : BasicConstructibleSetData (Localization.Away c)) ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x })
      T₁;
  let 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₂;
  comap Polynomial.C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) = (S₁ ∪ S₂).toSet
refine_2 refine_2₁ :
  let S₁ : Finset (BasicConstructibleSetData R) :=
    Finset.image (fun (x : BasicConstructibleSetData (Localization.Away c)) ↦ { f := c * f₁ x.f, n := x.n, g := g₁ x })
      T₁;
  let 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₂;
  ∀ C ∈ S₁ ∪ S₂,
    C.n ≤ e.degBound ∧ ∀ (i : Fin C.n), C.g i ∈ HPow.hPow (α := Submodule R₀ R) (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

Tactic:
classical
  let S₁ : Finset (BasicConstructibleSetData R) := T₁.image fun x ↦ ⟨c * f₁ x.f, _, g₁ x⟩
  let S₂ : Finset (BasicConstructibleSetData R) := T₂.image fun x ↦ ⟨f₂ x.f, _, Fin.cons c (g₂ x)⟩
  refine ⟨S₁ ∪ S₂, ?_, ?_⟩
  · calc
      comap Polynomial.C '' (zeroLocus (.range e) \ zeroLocus {f})
        = comap q₁ '' (comap Polynomial.C ''
            (comap (mapRingHom q₁.toRingHom) ⁻¹' (zeroLocus (.range e) \ zeroLocus {f}))) ∪
          comap q₂ '' (comap Polynomial.C ''
            (comap (mapRingHom q₂.toRingHom) ⁻¹' (zeroLocus (.range e) \ zeroLocus {f}))) :=
        Set.image_of_range_union_range_eq_univ (by ext; simp) (by ext; simp)
          (by rw [Ideal.Quotient.mkₐ_toRingHom,
            ← range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk,
            RingHom.algebraMap_toAlgebra]; exact Set.union_compl_self _) _
      _ = (⋃ C ∈ S₁, C.toSet) ∪ ⋃ C ∈ S₂, C.toSet := ?_
      _ = ⋃ C ∈ S₁ ∪ S₂, C.toSet := by
        simpa using (Set.biUnion_union (SetLike.coe S₁) S₂ _).symm
    congr 1
    · convert! congr(comap q₁.toRingHom '' $hT₁)
      · dsimp only [e₁]
        rw [Set.preimage_diff, preimage_comap_zeroLocus, preimage_comap_zeroLocus,
          Set.image_singleton, Pi.smul_def, ← Set.smul_set_range, Set.range_comp]
        congr 1
        refine (PrimeSpectrum.zeroLocus_smul_of_isUnit (.map _ ?_) _).symm
        exact isUnit_iff_exists_inv'.mpr ⟨_, IsLocalization.Away.mul_invSelf c⟩
      · rw [ConstructibleSetData.toSet, Set.image_iUnion₂]
        simp_rw [← Finset.mem_coe, S₁, Finset.coe_image, Set.biUnion_image]
        congr! with x hxT₁
        apply Set.injOn_preimage subset_rfl (f := comap q₁.toRingHom)
        · dsimp only [q₁, AlgHom.toRingHom_eq_coe]
          rw [IsScalarTower.coe_toAlgHom,
            localization_away_comap_range (S := Localization.Away c) (r := c),
            BasicConstructibleSetData.toSet, sdiff_eq, ← basicOpen_eq_zeroLocus_compl,
            basicOpen_mul]
          exact Set.inter_subset_right.trans Set.inter_subset_left
        · exact Set.image_subset_range ..
        · rw [BasicConstructibleSetData.toSet, BasicConstructibleSetData.toSet, Set.preimage_diff,
            preimage_comap_zeroLocus, preimage_comap_zeroLocus, Set.preimage_image_eq]
          swap; · exact localization_comap_injective _ (.powers c)
          simp only [AlgHom.toLinearMap_apply] at hq₁g₁
          simp only [← Set.range_comp, comp_def, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
            hq₁g₁ _ hxT₁, Set.image_singleton, map_mul, ← hf₁, mul_comm x.1, ← mul_assoc,
            ← pow_succ']
          simp only [← smul_eq_mul, ← Set.smul_set_range, ← Set.smul_set_singleton,
            zeroLocus_smul_of_isUnit ((isUnit_of_invertible (q₁ c)).pow _)]
    · convert! congr(comap q₂.toRingHom '' $hT₂)
      · rw [Set.preimage_diff, preimage_comap_zeroLocus, preimage_comap_zeroLocus,
          Set.image_singleton, Set.range_comp, AlgHom.toRingHom_eq_coe]
      · rw [ConstructibleSetData.toSet, Set.image_iUnion₂]
        simp_rw [← Finset.mem_coe, S₂, Finset.coe_image, Set.biUnion_image]
        congr! 3 with x hxT₂
        apply Set.injOn_preimage subset_rfl (f := comap q₂.toRingHom)
        · rw [range_comap_of_surjective _ _ q₂_surjective]
          simp only [AlgHom.toRingHom_eq_coe, Ideal.Quotient.mkₐ_ker, zeroLocus_span, q₂]
          exact Set.diff_subset.trans (zeroLocus_anti_mono (by simp))
        · exact Set.image_subset_range _ _
        · simp only [AlgHom.toLinearMap_apply] at hq₂g₂
          have : q₂ c = 0 := by simp [q₂]
          simp only [BasicConstructibleSetData.toSet, Set.preimage_diff, preimage_comap_zeroLocus,
            preimage_comap_zeroLocus,
            Set.preimage_image_eq _ (comap_injective_of_surjective _ q₂_surjective)]
          simp only [Fin.range_cons, Set.image_singleton, Set.image_insert_eq,
            ← Set.range_comp, comp_def]
          simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, hq₂g₂ _ hxT₂, hf₂]
          rw [← Set.union_singleton, zeroLocus_union,
            this, zeroLocus_singleton_zero, Set.inter_univ]
  · simp only [Finset.mem_union, forall_and, or_imp, Finset.forall_mem_image, S₁, S₂]
    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 _)⟩
    · norm_cast
      calc
        span R₀ ({c} ∪ ⋃ i, coeff(e i)) ^ e₁.powBound
        _ ≤ span R₀ (⋃ i, coeff(e i)) ^ e₁.powBound := by
          gcongr; simpa [Set.insert_subset_iff] using ⟨_, _, hi.symm⟩
        _ ≤ e.coeffSubmodule R₀ ^ e.powBound := by
          unfold coeffSubmodule powBound
          gcongr
          · exact one_le_coeffSubmodule
          · exact Set.subset_union_right
          · lia
    · exact le_self_pow one_le_coeffSubmodule powBound_ne_zero <| subset_span <| .inr <| by
        simpa using ⟨_, _, hi.symm⟩
    · unfold powBound
      gcongr
      · exact one_le_coeffSubmodule
      · lia

Premises used: PrimeSpectrum.zeroLocus_anti_mono, Iff.mpr, _private.0.ChevalleyThm.PolynomialC.InductionObj.val, Set.range_comp, Polynomial.C, PrimeSpectrum.BasicConstructibleSetData.toSet, AlgHom.coe_toRingHom, Set.diff_subset, range_comap_of_surjective, Set.image_singleton, PrimeSpectrum.zeroLocus, isUnit_of_invertible, RingHom.coe_coe, PrimeSpectrum.zeroLocus_span, PrimeSpectrum.basicOpen_mul, Set.inter_univ, mul_assoc, PrimeSpectrum.preimage_comap_zeroLocus, Localization.Away, AlgHom.toLinearMap_apply, Set.injOn_preimage, Finset.coe_image, HasSubset.Subset.trans, Set.image_subset_range, Set.image_of_range_union_range_eq_univ, PrimeSpectrum.zeroLocus_union, sdiff_eq, Set.inter_subset_left, Finset.forall_mem_image, IsScalarTower.coe_toAlgHom, or_imp, _private.0.ChevalleyThm.PolynomialC.InductionObj.powBound, Set.image_iUnion₂, IsLocalization.Away.mul_invSelf, IsUnit.pow, Polynomial.coeff, Ideal.Quotient.mkₐ_ker, SDiff.sdiff, map_mul, Function.comp_def, PrimeSpectrum.zeroLocus_smul_of_isUnit, _private.0.ChevalleyThm.PolynomialC.InductionObj.one_le_coeffSubmodule, Fin.range_cons, Set.preimage, PrimeSpectrum.localization_comap_injective, Set.smul_set_singleton, AlgHom.toRingHom, Set.smul_set_range, Polynomial.mapRingHom, AlgHom.toRingHom_eq_coe, Submonoid.powers, Exists.intro, Submodule.span, PrimeSpectrum.comap_injective_of_surjective, PrimeSpectrum.basicOpen_eq_zeroLocus_compl, Set.preimage_image_eq, Set.image, Finset.mem_union, IsUnit.map, Set.image_insert_eq, Submodule.subset_span, Set.range, smul_eq_mul, Union.union, PrimeSpectrum.comap, le_self_pow, Singleton.singleton, Pi.smul_def, Eq.symm, Set.union_singleton, DFunLike.coe, PrimeSpectrum.zeroLocus_singleton_zero, Set.iUnion, Finset.mem_coe, PrimeSpectrum.ConstructibleSetData.toSet, PrimeSpectrum.localization_away_comap_range, subset_rfl, Set.preimage_diff, pow_succ', _private.0.ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule, Set.biUnion_image, Set.inter_subset_right, forall_and, _private.0.ChevalleyThm.PolynomialC.InductionObj.powBound_ne_zero, isUnit_iff_exists_inv'