awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i_1 : ℕ
hi_1 : i_1 ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
hi : p.natDegree < i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i

Tactic:
simp [coeff_eq_zero_of_natDegree_lt hi, hi.ne']

Premises used: LT.lt.ne', Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
⊢ map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree

Tactic:
have : p.map (Ideal.Quotient.mk P) = X ^ p.natDegree := by
    ext i
    obtain hi | rfl | hi := lt_trichotomy i p.natDegree
    · simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using hPJ (Ideal.subset_span ⟨_, hi, rfl⟩)
    · simp [hp]
    · simp [coeff_eq_zero_of_natDegree_lt hi, hi.ne']
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
obtain :
  ∀ (j : ℕ) (hj : j ≤ p.natDegree) (a : (R ⧸ P)[X]ˣ)
    (ha : map (Ideal.Quotient.mk P) q * (↑a : (R ⧸ P)[X]) = HPow.hPow (α := (R ⧸ P)[X]) X j), q.coeff i ∈ P
⊢ q.coeff i ∈ P

Tactic:
obtain ⟨j, hj, a, ha⟩ :=
    (dvd_prime_pow (prime_X (R := R ⧸ P)) _).mp (this ▸ map_dvd (Ideal.Quotient.mk P) H)

Premises used: Iff.mp, dvd_prime_pow, Polynomial.prime_X
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
ha : map (Ideal.Quotient.mk P) q * (↑a : (R ⧸ P)[X]) = HPow.hPow (α := (R ⧸ P)[X]) X j
obtain : ∀ (r : R ⧸ P) (hr : IsUnit r) (e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])), q.coeff i ∈ P
⊢ q.coeff i ∈ P

Tactic:
obtain ⟨r, hr, e⟩ := isUnit_iff.mp a⁻¹.isUnit

Premises used: Polynomial.isUnit_iff, Inv.inv, Iff.mp, Units.isUnit
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
ha : map (Ideal.Quotient.mk P) q * (↑a : (R ⧸ P)[X]) = HPow.hPow (α := (R ⧸ P)[X]) X j
r : R ⧸ P
hr : IsUnit r
e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])
rw :
  ∀ (r : R ⧸ P)
    (ha :
      map (Ideal.Quotient.mk P) q =
        HMul.hMul (β := (R ⧸ P)[X]) (HPow.hPow (α := (R ⧸ P)[X]) X j) ((C : (a : R ⧸ P) → (R ⧸ P)[X]) r : (R ⧸ P)[X]))
    (hr : IsUnit r) (e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])), q.coeff i ∈ P
⊢ q.coeff i ∈ P

Tactic:
rw [← Units.eq_mul_inv_iff_mul_eq, ← e] at ha

Premises used: Units.eq_mul_inv_iff_mul_eq
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
r : R ⧸ P
ha :
  map (Ideal.Quotient.mk P) q =
    HMul.hMul (β := (R ⧸ P)[X]) (HPow.hPow (α := (R ⧸ P)[X]) X j) ((C : (a : R ⧸ P) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
hr : IsUnit r
e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])
⊢ j = q.natDegree

Tactic:
simpa [hq.natDegree_map, hr.ne_zero] using congr(($ha).natDegree).symm

Premises used: congrArg, id, Polynomial.Monic.natDegree_map, IsUnit.ne_zero, Polynomial.natDegree, Eq.symm
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
r : R ⧸ P
ha :
  map (Ideal.Quotient.mk P) q =
    HMul.hMul (β := (R ⧸ P)[X]) (HPow.hPow (α := (R ⧸ P)[X]) X j) ((C : (a : R ⧸ P) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
hr : IsUnit r
e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])
⊢ q.natDegree ≤ p.natDegree

Tactic:
obtain rfl : j = q.natDegree := by
    simpa [hq.natDegree_map, hr.ne_zero] using congr(($ha).natDegree).symm

Premises used: Polynomial.natDegree, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
j : ℕ
hj : j ≤ p.natDegree
a : (R ⧸ P)[X]ˣ
r : R ⧸ P
ha :
  map (Ideal.Quotient.mk P) q =
    HMul.hMul (β := (R ⧸ P)[X]) (HPow.hPow (α := (R ⧸ P)[X]) X j) ((C : (a : R ⧸ P) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
hr : IsUnit r
e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])
hj₁ : q.natDegree ≤ p.natDegree
⊢ map (Ideal.Quotient.mk P) q =
    HMul.hMul (β := (R ⧸ P)[X]) (HPow.hPow (α := (R ⧸ P)[X]) X q.natDegree)
      ((C : (a : R ⧸ P) → (R ⧸ P)[X]) r : (R ⧸ P)[X])

Tactic:
obtain rfl : j = q.natDegree := by
    simpa [hq.natDegree_map, hr.ne_zero] using congr(($ha).natDegree).symm

Premises used: Polynomial.natDegree, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i : ℕ
hi : i ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
this : map (Ideal.Quotient.mk P) p = HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree
a : (R ⧸ P)[X]ˣ
r : R ⧸ P
hr : IsUnit r
e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])
hj : q.natDegree ≤ p.natDegree
ha :
  map (Ideal.Quotient.mk P) q =
    HMul.hMul (β := (R ⧸ P)[X]) (HPow.hPow (α := (R ⧸ P)[X]) X q.natDegree)
      ((C : (a : R ⧸ P) → (R ⧸ P)[X]) r : (R ⧸ P)[X])
⊢ q.coeff i ∈ P

Tactic:
simpa [hi, Ideal.Quotient.eq_zero_iff_mem] using congr(($ha).coeff i)

Premises used: Ideal.Quotient.eq_zero_iff_mem
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
⊢ IsDomain R

Tactic:
have := (FaithfulSMul.algebraMap_injective R S).isDomain
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
exists_ideal_le_liesOver_of_lt :
  ∀ {p : Ideal R} [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ Algebra.HasGoingDown R S

Tactic:
constructor
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
exists_ideal_le_liesOver_of_lt :
  ∀ [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ ∀ [p.IsPrime] (Q : Ideal S) [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
_
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
exists_ideal_le_liesOver_of_lt : ∀ [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ ∀ [Q.IsPrime], p < Ideal.under R Q → ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
_
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this_1 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p) ≤ p
obtain :
  ∀ (P : Ideal SQ) (hP : P.IsPrime) (e : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) P = p),
    ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, hP, e⟩ :=
      (Ideal.comap_map_eq_self_iff_of_isPrime _).mp (this.antisymm Ideal.le_comap_map)

Premises used: Ideal.comap_map_eq_self_iff_of_isPrime, LE.le.antisymm, Ideal.le_comap_map, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this_1 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p) ≤ p
P : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) P = p
rw : p = Ideal.under R P
rw₁ rw₂ : Eq (α := Ideal R) (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) P) (Ideal.under R P)
⊢ p = Ideal.under R (Ideal.under S P)

Tactic:
rw [Ideal.under_under, ← e]

Premises used: Ideal.under_under
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this_1 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p) ≤ p
P : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) P = p
refine : Ideal.under S P ≤ Q
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
refine ⟨P.under S, ?_, inferInstance, ⟨by rw [Ideal.under_under, ← e]⟩⟩
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this_1 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p) ≤ p
P : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) P = p
⊢ Ideal.under S P ≤ Q

Tactic:
(Ideal.comap_mono (IsLocalRing.le_maximalIdeal_of_isPrime P)).trans_eq
      Localization.AtPrime.under_maximalIdeal

Premises used: LE.le.trans_eq, Set.Mem, Localization.AtPrime.under_maximalIdeal, Ideal.comap_mono, IsLocalRing.le_maximalIdeal_of_isPrime
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this_1 : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p) ≤ p
P : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) P = p
⊢ Ideal.under S P ≤ Q

Tactic:
exact (Ideal.comap_mono (IsLocalRing.le_maximalIdeal_of_isPrime P)).trans_eq
      Localization.AtPrime.under_maximalIdeal

Premises used: LE.le.trans_eq, Localization.AtPrime.under_maximalIdeal, Ideal.comap_mono, IsLocalRing.le_maximalIdeal_of_isPrime
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
exists_ideal_le_liesOver_of_lt :
  Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p) ≤ p
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p

Tactic:
suffices (p.map (algebraMap _ SQ)).comap (algebraMap _ SQ) ≤ p by
    obtain ⟨P, hP, e⟩ :=
      (Ideal.comap_map_eq_self_iff_of_isPrime _).mp (this.antisymm Ideal.le_comap_map)
    refine ⟨P.under S, ?_, inferInstance, ⟨by rw [Ideal.under_under, ← e]⟩⟩
    exact (Ideal.comap_mono (IsLocalRing.le_maximalIdeal_of_isPrime P)).trans_eq
      Localization.AtPrime.under_maximalIdeal
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
⊢ ∃ (a : S), Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a) ∧ a ∉ Q

Tactic:
simpa [Algebra.smul_def, IsScalarTower.algebraMap_eq R S SQ, ← Ideal.map_map,
      IsLocalization.mem_map_algebraMap_iff Q.primeCompl, ← map_mul] using hx

Premises used: map_mul, Ideal.map_map, IsScalarTower.algebraMap_eq, Algebra.smul_def, Ideal.primeCompl, IsLocalization.mem_map_algebraMap_iff
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
exists_ideal_le_liesOver_of_lt :
  ∀ (a : S) (ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)) (haQ : a ∉ Q),
    x ∈ p
⊢ x ∈ p

Tactic:
obtain ⟨a, ha, haQ⟩ : ∃ a, x • a ∈ Ideal.map (algebraMap R S) p ∧ a ∉ Q := by
    simpa [Algebra.smul_def, IsScalarTower.algebraMap_eq R S SQ, ← Ideal.map_map,
      IsLocalization.mem_map_algebraMap_iff Q.primeCompl, ← map_mul] using hx

Premises used: Algebra.algebraMap, Ideal.map
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
exists_ideal_le_liesOver_of_lt :
  ∀ (f : R[X]) (hfm : f.Monic) (hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S))
    (hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p), x ∈ p
⊢ x ∈ p

Tactic:
obtain ⟨f, hfm, hfa, hf⟩ := exists_monic_aeval_eq_zero_forall_mem_of_mem_map ha

Premises used: Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
set :
  let g : R[X] := minpoly R a;
  ∃ (i : ℕ), i ≠ g.natDegree ∧ g.coeff i ∉ p
⊢ ∃ (i : ℕ), i ≠ natDegree (minpoly R a) ∧ coeff (minpoly R a) i ∉ p

Tactic:
set g := minpoly R a

Premises used: minpoly
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
g : R[X] := minpoly R a
by_contra! : ∀ (H : ∀ (i : ℕ) (_ : i ≠ g.natDegree), g.coeff i ∈ p), False
⊢ ∃ (i : ℕ), i ≠ g.natDegree ∧ g.coeff i ∉ p

Tactic:
by_contra! H
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
g : R[X] := minpoly R a
H : ∀ (i : ℕ) (_ : i ≠ g.natDegree), g.coeff i ∈ p
a₁ : ∀ (i : ℕ), (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i
⊢ map (Ideal.Quotient.mk p) g = HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree

Tactic:
ext i
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
g : R[X] := minpoly R a
H : ∀ (i : ℕ) (_ : i ≠ g.natDegree), g.coeff i ∈ p
i : ℕ
a₁ :
  ∀ (hi : i < g.natDegree), (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i
a₂ : (map (Ideal.Quotient.mk p) g).coeff g.natDegree = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff g.natDegree
a₃ :
  ∀ (hi : g.natDegree < i), (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i

Tactic:
obtain hi | rfl | hi := lt_trichotomy i g.natDegree

Premises used: Polynomial.natDegree, rfl, lt_trichotomy
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
g : R[X] := minpoly R a
H : ∀ (i : ℕ) (_ : i ≠ g.natDegree), g.coeff i ∈ p
i : ℕ
hi : i < g.natDegree
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i

Tactic:
simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using H _ hi.ne

Premises used: Ideal.Quotient.eq_zero_iff_mem, LT.lt.ne
-- Module: Mathlib.RingTheory.IntegralClosure.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain S
inst_4 : FaithfulSMul R S
inst_5 : Algebra.IsIntegral R S
inst_6 : IsIntegrallyClosed R
this : IsDomain R
p : Ideal R
inst_7 : p.IsPrime
Q : Ideal S
inst_8 : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
x : R
hx :
  Membership.mem (γ := Submodule R R)
    (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p)) x
a : S
ha : Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p) (x • a)
haQ : a ∉ Q
f : R[X]
hfm : f.Monic
hfa : Eq.{u_2 + 1} (α := S) ((aeval (x • a) : (a : R[X]) → S) f : S) (0 : S)
hf : ∀ (i : ℕ), i ≠ f.natDegree → f.coeff i ∈ p
g : R[X] := minpoly R a
H : ∀ (i : ℕ) (_ : i ≠ g.natDegree), g.coeff i ∈ p
⊢ (map (Ideal.Quotient.mk p) g).coeff g.natDegree = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff g.natDegree

Tactic:
simp [g, minpoly.monic (Algebra.IsIntegral.isIntegral _)]

Premises used: Algebra.IsIntegral.isIntegral, minpoly.monic