awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : g.natDegree < i
⊢ (map (Ideal.Quotient.mk p) g).coeff i = (HPow.hPow (α := (R ⧸ p)[X]) X g.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
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

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']
-- 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
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
⊢ 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:
simpa [← Ideal.Quotient.algebraMap_eq, aeval_algebraMap_apply, g] using
        congr(aeval (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p) a) $this).symm

Premises used: Algebra.algebraMap, congrArg, Ideal.Quotient.mk, Ideal.Quotient.algebraMap_eq, id, Ideal.map, Polynomial.aeval, Eq.symm, DFunLike.coe, Polynomial.aeval_algebraMap_apply
-- 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
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
⊢ 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
-- 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
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_2 : map (Ideal.Quotient.mk p) g = HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree
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))
⊢ False

Tactic:
haQ (‹Q.IsPrime›.mem_of_pow_mem _
      (Ideal.map_le_iff_le_comap.mpr hpQ.le (Ideal.Quotient.eq_zero_iff_mem.mp this)))

Premises used: Iff.mpr, Ideal.IsPrime.mem_of_pow_mem, LT.lt.le, Ideal.Quotient.eq_zero_iff_mem, Ideal.map_le_iff_le_comap, 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
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_2 : map (Ideal.Quotient.mk p) g = HPow.hPow (α := (R ⧸ p)[X]) X g.natDegree
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))
⊢ False

Tactic:
exact haQ (‹Q.IsPrime›.mem_of_pow_mem _
      (Ideal.map_le_iff_le_comap.mpr hpQ.le (Ideal.Quotient.eq_zero_iff_mem.mp this)))

Premises used: Iff.mpr, Ideal.IsPrime.mem_of_pow_mem, LT.lt.le, Ideal.Quotient.eq_zero_iff_mem, Ideal.map_le_iff_le_comap, 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 : 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
exists_ideal_le_liesOver_of_lt : ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (hip : coeff (minpoly R a) i ∉ p), x ∈ p
⊢ x ∈ p

Tactic:
obtain ⟨i, hi, hip⟩ : ∃ i ≠ (minpoly R a).natDegree, (minpoly R a).coeff i ∉ p := by
    set g := minpoly R a
    by_contra! H
    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']
    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
    exact haQ (‹Q.IsPrime›.mem_of_pow_mem _
      (Ideal.map_le_iff_le_comap.mpr hpQ.le (Ideal.Quotient.eq_zero_iff_mem.mp this)))

Premises used: minpoly, Polynomial.natDegree
-- 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
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
pos : ∀ (hx0 : x = 0), x ∈ p
neg : ∀ (hx0 : ¬x = 0), x ∈ p
⊢ x ∈ p

Tactic:
by_cases hx0 : x = 0
-- 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
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : x = 0
⊢ x ∈ p

Tactic:
simp [hx0]
-- 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
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
⊢ ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R (x • a))),
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x}))
      (coeff (minpoly R (x • a)) i)

Tactic:
have := Polynomial.coeff_mem_radical_span_coeff_of_dvd _ _ hfm
    (minpoly.monic (Algebra.IsIntegral.isIntegral _))
    (minpoly.isIntegrallyClosed_dvd (Algebra.IsIntegral.isIntegral _) hfa)
-- 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
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
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R (x • a))),
    Membership.mem (γ := Ideal R) (Ideal.radical (Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x}))
      (coeff (minpoly R (x • a)) i)
⊢ ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (p : Submodule R R),
    Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p →
      Ideal.IsPrime p → coeff (minpoly R a) i * x ^ (natDegree (minpoly R a) - i) ∈ p

Tactic:
simp only [IsIntegrallyClosed.minpoly_smul hx0 (Algebra.IsIntegral.isIntegral _),
    natDegree_scaleRoots, coeff_scaleRoots, Ideal.radical_eq_sInf, Submodule.mem_sInf,
    Set.mem_setOf_eq, and_imp] at this

Premises used: Algebra.IsIntegral.isIntegral, and_imp, Polynomial.coeff_scaleRoots, Polynomial.natDegree_scaleRoots, Set.mem_setOf_eq, Ideal.radical_eq_sInf, Submodule.mem_sInf, IsIntegrallyClosed.minpoly_smul
-- 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
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
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (p : Submodule R R),
    Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p →
      Ideal.IsPrime p → coeff (minpoly R a) i * x ^ (natDegree (minpoly R a) - i) ∈ p
⊢ x ∈ p

Tactic:
‹p.IsPrime›.mem_of_pow_mem _ ((‹p.IsPrime›.mem_or_mem
    (this i hi p ?_ inferInstance)).resolve_left hip)

Premises used: Set.Mem, Ideal.IsPrime.mem_of_pow_mem, inferInstance, Or.resolve_left, Ideal.IsPrime.mem_or_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
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
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (p : Submodule R R),
    Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p →
      Ideal.IsPrime p → coeff (minpoly R a) i * x ^ (natDegree (minpoly R a) - i) ∈ p
neg : Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p
⊢ x ∈ p

Tactic:
refine ‹p.IsPrime›.mem_of_pow_mem _ ((‹p.IsPrime›.mem_or_mem
    (this i hi p ?_ inferInstance)).resolve_left hip)

Premises used: Ideal.IsPrime.mem_of_pow_mem, inferInstance, Or.resolve_left, Ideal.IsPrime.mem_or_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
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
i : ℕ
hi : i ≠ natDegree (minpoly R a)
hip : coeff (minpoly R a) i ∉ p
hx0 : ¬x = 0
this :
  ∀ (i : ℕ) (hi : i ≠ natDegree (minpoly R a)) (p : Submodule R R),
    Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p →
      Ideal.IsPrime p → coeff (minpoly R a) i * x ^ (natDegree (minpoly R a) - i) ∈ p
⊢ Ideal.span {x : R | ∃ i < f.natDegree, f.coeff i = x} ≤ p

Tactic:
simp +contextual [Ideal.span_le, Set.subset_def, LT.lt.ne, hf]

Premises used: Ideal.span_le, Set.subset_def, LT.lt.ne
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
⊢ IsIntegrallyClosedIn R A

Tactic:
⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩

Premises used: IsIntegralClosure.mk, Iff.intro, Function.Injective.of_comp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
refine_1 :
  Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
refine_2 : ∀ {x : A} (hx : IsIntegral R x), ∃ (y : R), (algebraMap R A : (a : R) → A) y = x
refine_3 : ∀ {x : A}, (∃ (y : R), (algebraMap R A : (a : R) → A) y = x) → IsIntegral R x
⊢ IsIntegrallyClosedIn R A

Tactic:
refine ⟨Function.Injective.of_comp (f := f) ?_, fun hx => ?_, ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)

Tactic:
inj
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
h :
  Eq (α := R → B)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
    (⇑(algebraMap R B) : (a : R) → B)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))

Tactic:
convert! inj
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
B : Type u_3
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := B) (⇑(algebraMap R B) : (a : R) → B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ (y : R), (algebraMap R B : (a : R) → B) y = x
⊢ Eq (α := R → B)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := A) (⇑f : (a : A) → B) (⇑(algebraMap R A) : (a : R) → A))
    (⇑(algebraMap R B) : (a : R) → B)

Tactic:
aesop