awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧
    (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥

Tactic:
⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩

Premises used: mt, And.intro, Iff.mp, mul_le_mul', Ideal.mul_eq_bot, le_trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h : (M + A ∙ x) * (M + A ∙ y) ≤ M
h₁ : ¬((Multiset.map asIdeal Wx).prod = ⊥ ∨ (Multiset.map asIdeal Wy).prod = ⊥)
⊢ (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≤ M ∧
    (Multiset.map asIdeal Wx).prod * (Multiset.map asIdeal Wy).prod ≠ ⊥

Tactic:
refine ⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h : M * (M + A ∙ y) + (A ∙ x) * (M + A ∙ y) ≤ M
⊢ (M + A ∙ x) * (M + A ∙ y) ≤ M

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h : (A ∙ x) * (M + A ∙ y) ≤ M
⊢ M * (M + A ∙ y) + (A ∙ x) * (M + A ∙ y) ≤ M

Tactic:
apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_right)

Premises used: Ideal.mul_le_right, sup_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h : (A ∙ x) * M + HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M
⊢ (A ∙ x) * (M + A ∙ y) ≤ M

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h : HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M
⊢ (A ∙ x) * M + HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M

Tactic:
apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_left)

Premises used: Ideal.mul_le_left, sup_le
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
h : span A (HMul.hMul (α := Set A) {x} {y}) ≤ M
h₁ : A ∙ x * y ≤ M
h₂ h₃ h₄ h₅ : x * y ∈ M
⊢ HMul.hMul (α := Ideal A) (A ∙ x) (A ∙ y) ≤ M

Tactic:
rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]

Premises used: Submodule.span_mul_span, Submodule.span_singleton_le_iff_mem, Set.singleton_mul_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx_1 : x ∉ M
y : A
hy : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
hx : (Multiset.map asIdeal Wx).prod = ⊥
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
M : Ideal A
hgt :
  ∀ J > M,
    ∀ (h_nzI : J ≠ ⊥),
      ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
h_nzI : M ≠ ⊥
hA_nont : Nontrivial A
h_topM : ¬M = ⊤
h_prM : ¬M.IsPrime
x : A
hx : x ∉ M
y : A
hy_1 : y ∉ M
h_xy : x * y ∈ M
lt_add : ∀ z ∉ M, M < M + A ∙ z
Wx : Multiset (PrimeSpectrum A)
h_Wx_le : (Multiset.map asIdeal Wx).prod ≤ M + A ∙ x
h_Wx_ne_1 : (Multiset.map asIdeal Wx).prod ≠ ⊥
Wy : Multiset (PrimeSpectrum A)
h_Wy_le : (Multiset.map asIdeal Wy).prod ≤ M + A ∙ y
h_Wx_ne : (Multiset.map asIdeal Wy).prod ≠ ⊥
hy : (Multiset.map asIdeal Wy).prod = ⊥
⊢ False

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Spectrum.Prime.Basic
Goal:
A : Type u
inst : CommRing A
inst_1 : IsDomain A
inst_2 : IsNoetherianRing A
h_fA : ¬IsField A
I : Ideal A
h_nzI : I ≠ ⊥
hgt :
  ∀ (M : Submodule A A)
    (hgt :
      ∀ J > M,
        ∀ (h_nzI : J ≠ ⊥),
          ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ J ∧ (Multiset.map asIdeal Z).prod ≠ ⊥)
    (h_nzI : M ≠ ⊥),
    ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ M ∧ (Multiset.map asIdeal Z).prod ≠ ⊥
⊢ ∃ (Z : Multiset (PrimeSpectrum A)), (Multiset.map asIdeal Z).prod ≤ I ∧ (Multiset.map asIdeal Z).prod ≠ ⊥

Tactic:
induction I using IsNoetherian.induction with | hgt M hgt =>
  change Ideal A at M
  have hA_nont : Nontrivial A := IsDomain.toNontrivial
  by_cases h_topM : M = ⊤
  · rcases h_topM with rfl
    obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ p : Ideal A, p ≠ ⊥ ∧ p.IsPrime := by
      apply Ring.not_isField_iff_exists_prime.mp h_fA
    use ({⟨p_id, h_pp⟩} : Multiset (PrimeSpectrum A)), le_top
    rwa [Multiset.map_singleton, Multiset.prod_singleton]
  by_cases h_prM : M.IsPrime
  · use ({⟨M, h_prM⟩} : Multiset (PrimeSpectrum A))
    rw [Multiset.map_singleton, Multiset.prod_singleton]
    exact ⟨le_rfl, h_nzI⟩
  obtain ⟨x, hx, y, hy, h_xy⟩ := (Ideal.not_isPrime_iff.mp h_prM).resolve_left h_topM
  have lt_add : ∀ z ∉ M, M < M + span A {z} := by
    intro z hz
    refine lt_of_le_of_ne le_sup_left fun m_eq => hz ?_
    rw [m_eq]
    exact mem_sup_right (mem_span_singleton_self z)
  obtain ⟨Wx, h_Wx_le, h_Wx_ne⟩ := hgt (M + span A {x}) (lt_add _ hx) (ne_bot_of_gt (lt_add _ hx))
  obtain ⟨Wy, h_Wy_le, h_Wx_ne⟩ := hgt (M + span A {y}) (lt_add _ hy) (ne_bot_of_gt (lt_add _ hy))
  use Wx + Wy
  rw [Multiset.map_add, Multiset.prod_add]
  refine ⟨le_trans (mul_le_mul' h_Wx_le h_Wy_le) ?_, mt Ideal.mul_eq_bot.mp ?_⟩
  · rw [add_mul]
    apply sup_le (show M * (M + span A {y}) ≤ M from Ideal.mul_le_right)
    rw [mul_add]
    apply sup_le (show span A {x} * M ≤ M from Ideal.mul_le_left)
    rwa [span_mul_span, Set.singleton_mul_singleton, span_singleton_le_iff_mem]
  · rintro (hx | hy) <;> contradiction

Premises used: add_mul, IsNoetherian.induction, Multiset.map_singleton, Submodule.span_mul_span, Multiset.prod_singleton, Ideal, le_top, Multiset.prod_add, mul_add, Submodule.span_singleton_le_iff_mem, Singleton.singleton, Multiset.map_add, rfl, Set.singleton_mul_singleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
inst : CommRing R
s : Set (PrimeSpectrum R[X])
hs : IsConstructible s
obtain :
  ∀ (S : ConstructibleSetData R[X]) (hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet),
    IsConstructible (comap Polynomial.C '' S.toSet)
⊢ IsConstructible (comap Polynomial.C '' s)

Tactic:
obtain ⟨S, rfl⟩ := exists_constructibleSetData_iff.mpr hs

Premises used: Iff.mpr, PrimeSpectrum.exists_constructibleSetData_iff, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
inst : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet
⊢ ∀ C ∈ S, ∀ (j : Fin C.n) (k : ℕ), Membership.mem (γ := Submodule ℤ R) ⊤ ((C.g j).coeff k)

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
inst : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet
obtain :
  ∀ (T : ConstructibleSetData R) (hT : comap Polynomial.C '' S.toSet = T.toSet),
    IsConstructible (comap Polynomial.C '' S.toSet)
⊢ IsConstructible (comap Polynomial.C '' S.toSet)

Tactic:
obtain ⟨T, hT, -⟩ := ChevalleyThm.chevalley_polynomialC _ Submodule.mem_top S (by simp)

Premises used: ChevalleyThm.chevalley_polynomialC, Submodule.mem_top
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
inst : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet
T : ConstructibleSetData R
hT : comap Polynomial.C '' S.toSet = T.toSet
rw : IsConstructible (X := PrimeSpectrum R) T.toSet
⊢ IsConstructible (comap Polynomial.C '' S.toSet)

Tactic:
rw [hT]
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
inst : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet
T : ConstructibleSetData R
hT : comap Polynomial.C '' S.toSet = T.toSet
⊢ IsConstructible (X := PrimeSpectrum R) T.toSet

Tactic:
T.isConstructible_toSet

Premises used: PrimeSpectrum.ConstructibleSetData.isConstructible_toSet
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
inst : CommRing R
S : ConstructibleSetData R[X]
hs : IsConstructible (X := PrimeSpectrum R[X]) S.toSet
T : ConstructibleSetData R
hT : comap Polynomial.C '' S.toSet = T.toSet
⊢ IsConstructible (X := PrimeSpectrum R) T.toSet

Tactic:
exact T.isConstructible_toSet

Premises used: PrimeSpectrum.ConstructibleSetData.isConstructible_toSet
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsConstructible (comap f '' s)

Tactic:
hf.polynomial_induction
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ ↦ isConstructible_comap_C) ?_ ?_ f s hs

Premises used: RingHom.FinitePresentation.polynomial_induction, PrimeSpectrum.isConstructible_comap_C
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
refine_1 :
  ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_2) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) →
      Ideal.FG (RingHom.ker f) →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst S inst_2 f
refine_2 :
  ∀ (R : Type u_1) [inst : CommRing R] (S : Type u_1) [inst_2 : CommRing S] (T : Type u_2) [inst_3 : CommRing T]
    (f : R →+* S) (g : S →+* T),
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst S inst_2 f →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          S inst_2 T inst_3 g →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst T inst_3 (g.comp f)
⊢ IsConstructible (comap f '' s)

Tactic:
refine hf.polynomial_induction
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s))
    (fun _ _ _ ↦ isConstructible_comap_C) ?_ ?_ f s hs

Premises used: RingHom.FinitePresentation.polynomial_induction, PrimeSpectrum.isConstructible_comap_C
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S : Type u_2
inst : CommRing R_1
inst_1 : CommRing S
f : R_1 →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
refine_1 :
  ∀ [inst : CommRing R] (S : Type u_2) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) →
      Ideal.FG (RingHom.ker f) →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst S inst_2 f
⊢ ∀ [inst : CommRing R] (S : Type u_2) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) →
      Ideal.FG (RingHom.ker f) →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst S inst_2 f

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f : R_1 →+* S_1
hf : f.FinitePresentation
s : Set (PrimeSpectrum S_1)
hs : IsConstructible s
R : Type u_1
inst_2 : CommRing R
S : Type u_2
refine_1 :
  ∀ [inst : CommRing S] (f : R →+* S),
    Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) →
      Ideal.FG (RingHom.ker f) →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst_2 S inst f
⊢ ∀ [inst : CommRing S] (f : R →+* S),
    Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) →
      Ideal.FG (RingHom.ker f) →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst_2 S inst f

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf_1 : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_2
inst_3 : CommRing S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf' : Ideal.FG (RingHom.ker f)
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsConstructible (comap f '' s)

Tactic:
hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ f hf) ?_

Premises used: Topology.IsConstructible.image_of_isClosedEmbedding, PrimeSpectrum.isClosedEmbedding_comap_of_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf_1 : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_2
inst_3 : CommRing S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf' : Ideal.FG (RingHom.ker f)
s : Set (PrimeSpectrum S)
hs : IsConstructible s
refine_1 : IsRetrocompact (Set.range (comap f))ᶜ
⊢ IsConstructible (comap f '' s)

Tactic:
refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ f hf) ?_

Premises used: Topology.IsConstructible.image_of_isClosedEmbedding, PrimeSpectrum.isClosedEmbedding_comap_of_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf_1 : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_2
inst_3 : CommRing S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf' : Ideal.FG (RingHom.ker f)
s : Set (PrimeSpectrum S)
hs : IsConstructible s
refine_1 : IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(RingHom.ker f) : Set R))ᶜ
⊢ IsRetrocompact (Set.range (comap f))ᶜ

Tactic:
rw [range_comap_of_surjective _ f hf]

Premises used: range_comap_of_surjective
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf_1 : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_2
inst_3 : CommRing S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf' : Ideal.FG (RingHom.ker f)
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(RingHom.ker f) : Set R))ᶜ

Tactic:
isRetrocompact_zeroLocus_compl_of_fg hf'

Premises used: PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf_1 : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_2
inst_3 : CommRing S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hf' : Ideal.FG (RingHom.ker f)
s : Set (PrimeSpectrum S)
hs : IsConstructible s
⊢ IsRetrocompact (X := PrimeSpectrum R) (zeroLocus (↑(RingHom.ker f) : Set R))ᶜ

Tactic:
exact isRetrocompact_zeroLocus_compl_of_fg hf'

Premises used: PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S : Type u_2
inst : CommRing R_1
inst_1 : CommRing S
f : R_1 →+* S
hf : f.FinitePresentation
s : Set (PrimeSpectrum S)
hs : IsConstructible s
R : Type u_1
refine_2 :
  ∀ [inst : CommRing R] (S : Type u_1) [inst_2 : CommRing S] (T : Type u_2) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T),
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst S inst_2 f →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          S inst_2 T inst_3 g →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst T inst_3 (g.comp f)
⊢ ∀ [inst : CommRing R] (S : Type u_1) [inst_2 : CommRing S] (T : Type u_2) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T),
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst S inst_2 f →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          S inst_2 T inst_3 g →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst T inst_3 (g.comp f)

Tactic:
_