awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i_1 : ℕ
hi : i_1 ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
have a : ∀ (hi : i < p.natDegree), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
Tactic: obtain hi | rfl | hi := lt_trichotomy i p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i_1 : ℕ
hi : i_1 ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
a :
  ∀ (hi : i < p.natDegree), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
have a₁ : (map (Ideal.Quotient.mk P) p).coeff p.natDegree = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff p.natDegree
Tactic: obtain hi | rfl | hi := lt_trichotomy i p.natDegree
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
Goal:
R : Type u_1
inst : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
H : q ∣ p
i_1 : ℕ
hi : i_1 ≠ q.natDegree
P : Ideal R
hPJ : Ideal.span {x : R | ∃ i < p.natDegree, p.coeff i = x} ≤ P
hP : P.IsPrime
i : ℕ
a :
  ∀ (hi : i < p.natDegree), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
a₁ : (map (Ideal.Quotient.mk P) p).coeff p.natDegree = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff p.natDegree
⊢ (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
have a₂ : ∀ (hi : p.natDegree < i), (map (Ideal.Quotient.mk P) p).coeff i = (HPow.hPow (α := (R ⧸ P)[X]) X p.natDegree).coeff i
Tactic: obtain hi | rfl | hi := lt_trichotomy i p.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
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
⊢ q.coeff i ∈ P
have this : 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']
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ q.coeff i ∈ P
have 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
Tactic: obtain ⟨j, hj, a, ha⟩ :=
    (dvd_prime_pow (prime_X (R := R ⧸ P)) _).mp (this ▸ map_dvd (Ideal.Quotient.mk P) H)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ q.coeff i ∈ P
have obtain : ∀ (r : R ⧸ P) (hr : IsUnit r) (e : (C : (a : R ⧸ P) → (R ⧸ P)[X]) r = (↑a⁻¹ : (R ⧸ P)[X])), q.coeff i ∈ P
Tactic: obtain ⟨r, hr, e⟩ := isUnit_iff.mp a⁻¹.isUnit
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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])
⊢ q.coeff i ∈ P
have 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
Tactic: rw [← Units.eq_mul_inv_iff_mul_eq, ← e] at ha
Cleared hypotheses: ha, r, hr, e
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
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.coeff i ∈ P
have hj₁ : q.natDegree ≤ p.natDegree
Tactic: obtain rfl : j = q.natDegree := by
    simpa [hq.natDegree_map, hr.ne_zero] using congr(($ha).natDegree).symm
Cleared hypotheses: j, hj, ha
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
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
⊢ q.coeff i ∈ P
have 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])
Tactic: obtain rfl : j = q.natDegree := by
    simpa [hq.natDegree_map, hr.ne_zero] using congr(($ha).natDegree).symm
Cleared hypotheses: j, hj, ha
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
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
⊢ Algebra.HasGoingDown R S
have this : IsDomain R
Tactic: have := (FaithfulSMul.algebraMap_injective R S).isDomain
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ Algebra.HasGoingDown R S
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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 ≤ Q, P.IsPrime ∧ P.LiesOver p
have 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
Tactic: obtain ⟨P, hP, e⟩ :=
      (Ideal.comap_map_eq_self_iff_of_isPrime _).mp (this.antisymm Ideal.le_comap_map)
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ p = Ideal.under R (Ideal.under S P)
have rw : p = Ideal.under R P
Tactic: rw [Ideal.under_under, ← e]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ p = Ideal.under R (Ideal.under S P)
have rw₁ : Eq (α := Ideal R) (Ideal.comap (F := R →+* SQ) (algebraMap R SQ) P) (Ideal.under R P)
Tactic: rw [Ideal.under_under, ← e]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have refine : Ideal.under S P ≤ Q
Tactic: refine ⟨P.under S, ?_, inferInstance, ⟨by rw [Ideal.under_under, ← e]⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ ∃ P ≤ Q, P.IsPrime ∧ P.LiesOver p
have exists_ideal_le_liesOver_of_lt : Ideal.comap (F := R →+* SQ) (algebraMap R SQ) (Ideal.map (F := R →+* SQ) (algebraMap R SQ) p) ≤ 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
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ x ∈ p
have 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
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
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ x ∈ p
have 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
Tactic: obtain ⟨f, hfm, hfa, hf⟩ := exists_monic_aeval_eq_zero_forall_mem_of_mem_map ha
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ ∃ (i : ℕ), i ≠ g.natDegree ∧ g.coeff i ∉ p
have by_contra! : ∀ (H : ∀ (i : ℕ) (_ : i ≠ g.natDegree), g.coeff i ∈ p), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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 = HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree
have a₁ : ∀ (i : ℕ), (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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 : ℕ
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i
have a₁ : ∀ (hi : i < g.natDegree), (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
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i
have a₂ : (map (Ideal.Quotient.mk p) g).coeff g.natDegree = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff g.natDegree
Tactic: obtain hi | rfl | hi := lt_trichotomy i g.natDegree
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (goal)
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
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree).coeff i
have a₃ : ∀ (hi : g.natDegree < 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
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
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
⊢ False
have this₁ : map (Ideal.Quotient.mk p) g = HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree
Tactic: have : g.map (Ideal.Quotient.mk p) = X ^ g.natDegree := by
      ext i
      obtain hi | rfl | hi := lt_trichotomy i g.natDegree
      · simpa [hi.ne, Ideal.Quotient.eq_zero_iff_mem] using H _ hi.ne
      · simp [g, minpoly.monic (Algebra.IsIntegral.isIntegral _)]
      · simp [coeff_eq_zero_of_natDegree_lt hi, hi.ne']
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.GoingDown (hypothesis)
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
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
this : map (Ideal.Quotient.mk p) g = HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree
⊢ False
have this₁ : Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ Ideal.map (algebraMap R S) p)
      (a ^ natDegree (minpoly R a)) :
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
  (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
Tactic: have : Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) (a ^ (minpoly R a).natDegree) = 0 := by
      simpa [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, g] using
        congr(aeval (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) a) $this).symm