awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • z)
this : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have this₁ : Module.IsTorsionFree R L
Tactic: have : Module.IsTorsionFree R L := .trans_faithfulSMul R K L
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • z)
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have rw : ∀ (hz : Membership.mem (γ := Subalgebra R L) (AlgHom.range (aeval B.gen)) (p • z)) (this : Module.Finite K L),
  let P : R[X] := minpoly R B.gen;
  ∀ (hei : P.IsEisensteinAt (R ∙ p)) (hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0) (hP : P = minpoly R B.gen) (n : ℕ)
    (hn : B.dim = n.succ) (this : Module.IsTorsionFree R L), Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: rw [adjoin_singleton_eq_range_aeval] at hz
Cleared hypotheses: hz, this_1, P, hei, hndiv, hP, n, hn, this, x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) (AlgHom.range (aeval B.gen)) (p • z)
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have obtain : ∀ (Q₁ : R[X]) (hQ : (AlgHom.toRingHom (aeval B.gen) : (a : R[X]) → L) Q₁ = p • z),
  Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: obtain ⟨Q₁, hQ⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
hQ : (AlgHom.toRingHom (aeval B.gen) : (a : R[X]) → L) Q₁ = p • z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have hQ₁ : let Q := Q₁ %ₘ P;
Q = Q₁ %ₘ P
Tactic: set Q := Q₁ %ₘ P with hQ₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
hQ : (AlgHom.toRingHom (aeval B.gen) : (a : R[X]) → L) Q₁ = p • z
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
⊢ (aeval B.gen : (a : R[X]) → L) Q = p • z
have rw : ∀
  (hQ :
    (AlgHom.toRingHom (aeval B.gen) : (a : R[X]) → L)
        (Q₁ %ₘ minpoly R B.gen + minpoly R B.gen * (Q₁ /ₘ minpoly R B.gen)) =
      p • z),
  let Q := Q₁ %ₘ P;
  ∀ (hQ₁ : Q = Q₁ %ₘ P), (aeval B.gen : (a : R[X]) → L) Q = p • z
Tactic: rw [← modByMonic_add_div Q₁ (minpoly R B.gen)] at hQ
Cleared hypotheses: hQ, Q, hQ₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
hQ : (AlgHom.toRingHom (aeval B.gen) : (a : R[X]) → L) Q₁ = p • z
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have hQ₂ : (aeval B.gen : (a : R[X]) → L) Q = p • z
Tactic: replace hQ : aeval B.gen Q = p • z := by
    rw [← modByMonic_add_div Q₁ (minpoly R B.gen)] at hQ
    simpa using hQ
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have pos : ∀ (hQzero : Q = 0), Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: by_cases hQzero : Q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
pos : ∀ (hQzero : Q = 0), Membership.mem (γ := Subalgebra R L) R[B.gen] z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have neg : ∀ (hQzero : ¬Q = 0), Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: by_cases hQzero : Q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : Q = 0
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have hQ₂ : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L) ∨ z = 0
Tactic: simp only [hQzero, Algebra.smul_def, zero_eq_mul, aeval_zero] at hQ
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
hQ : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L) ∨ z = 0
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have pos : ∀ (H : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L)),
  Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: rcases hQ with H | H₁
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
hQ : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L) ∨ z = 0
pos :
  ∀ (H : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L)),
    Membership.mem (γ := Subalgebra R L) R[B.gen] z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have pos₁ : ∀ (H₁ : z = 0), Membership.mem (γ := Subalgebra R L) R[B.gen] z
Tactic: rcases hQ with H | H₁
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L)
⊢ Function.Injective.{u + 1, z + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
have rw : Function.Injective.{u + 1, z + 1} (α := R) (β := L)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)
Tactic: rw [algebraMap_eq R K L]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have this₁ : Function.Injective.{u + 1, z + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
Tactic: have : Function.Injective (algebraMap R L) := by
        rw [algebraMap_eq R K L]
        exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this_2 : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H : Eq.{z + 1} (α := L) ((algebraMap R L : (a : R) → L) p : L) (0 : L)
this : Function.Injective.{u + 1, z + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have pos : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : Q = 0
H₁ : z = 0
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have pos : Membership.mem (γ := Subalgebra R L) R[B.gen] 0
Tactic: rw [H₁]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z
have neg : ∀ i ∈ range (Q.natDegree + 1), p ∣ Q.coeff i
Tactic: refine mem_adjoin_of_dvd_coeff_of_dvd_aeval hp.ne_zero (fun i => ?_) hQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
⊢ p ∣ Q.coeff (j + 1)
have neg : p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
Tactic: convert! hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd (n := n) _ hndiv
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
have H : (Q₁ %ₘ minpoly R B.gen).degree < degree (minpoly R B.gen)
Tactic: have H := degree_modByMonic_lt Q₁ (minpoly.monic hBint)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (hypothesis)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : Q.degree < P.degree
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
have H₁ : j + 1 + 1 ≤ P.natDegree
Tactic: replace H := Nat.lt_iff_add_one_le.1
      (lt_of_lt_of_le
        (lt_of_le_of_lt (Nat.lt_iff_add_one_le.1 (Nat.lt_of_succ_lt_succ (mem_range.1 hj)))
          (lt_succ_self _)) (Nat.lt_iff_add_one_le.1 ((natDegree_lt_natDegree_iff hQzero).2 H)))
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
⊢ Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
have rw : 1 + Q.natDegree = j + 1 + (Q.natDegree - j)
Tactic: rw [← add_comm 1, ← add_comm 1, add_assoc, add_right_inj,
        ← Nat.add_sub_assoc (Nat.lt_of_succ_lt_succ (mem_range.1 hj)).le, add_comm,
        Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
rw : 1 + Q.natDegree = j + 1 + (Q.natDegree - j)
⊢ Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
have rw₁ : 1 + Q.natDegree = 1 + j + (Q.natDegree - j)
Tactic: rw [← add_comm 1, ← add_comm 1, add_assoc, add_right_inj,
        ← Nat.add_sub_assoc (Nat.lt_of_succ_lt_succ (mem_range.1 hj)).le, add_comm,
        Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
rw : 1 + Q.natDegree = j + 1 + (Q.natDegree - j)
rw₁ : 1 + Q.natDegree = 1 + j + (Q.natDegree - j)
⊢ Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
have rw₂ : 1 + Q.natDegree = 1 + (j + (Q.natDegree - j))
Tactic: rw [← add_comm 1, ← add_comm 1, add_assoc, add_right_inj,
        ← Nat.add_sub_assoc (Nat.lt_of_succ_lt_succ (mem_range.1 hj)).le, add_comm,
        Nat.add_sub_cancel]