awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
refine : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n
⊢ p ∣ Q.coeff 0

Tactic:
refine hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd (n := n) (?_ : _ ∣ _) hndiv

Premises used: Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
⊢ p ^ n.succ ∣
    Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n) *
      (↑(HPow.hPow (α := Rˣ) (-1) (n.succ * n)) : R)

Tactic:
(IsUnit.dvd_mul_right ⟨(-1) ^ (n.succ * n), rfl⟩).mpr this

Premises used: Iff.mpr, HMul.hMul, HPow.hPow, Exists.intro, IsUnit.dvd_mul_right, OfNat.ofNat, Nat.succ, Neg.neg, rfl
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
h :
  Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n =
    Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n) *
      (↑(HPow.hPow (α := Rˣ) (-1) (n.succ * n)) : R)
⊢ p ^ n.succ ∣ Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n

Tactic:
convert! (IsUnit.dvd_mul_right ⟨(-1) ^ (n.succ * n), rfl⟩).mpr this using 1

Premises used: Iff.mpr, HMul.hMul, HPow.hPow, Exists.intro, IsUnit.dvd_mul_right, OfNat.ofNat, Nat.succ, Neg.neg, rfl
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
h :
  Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n =
    Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n) *
      HPow.hPow (α := R) (-1) (n.succ * n)
⊢ Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n =
    Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n) *
      (↑(HPow.hPow (α := Rˣ) (-1) (n.succ * n)) : R)

Tactic:
push_cast
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
h :
  Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n =
    Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n * HPow.hPow (α := R) (-1) (n.succ * n * 2)
⊢ Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n =
    Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n) *
      HPow.hPow (α := R) (-1) (n.succ * n)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this_1 : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
this : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
⊢ Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n =
    Q.coeff 0 ^ n.succ * coeff (minpoly R B.gen) 0 ^ n * HPow.hPow (α := R) (-1) (n.succ * n * 2)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
p₁ : p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
⊢ p ∣ Q.coeff 0

Tactic:
suffices
      p ^ n.succ ∣ Q.coeff 0 ^ n.succ * ((-1) ^ (n.succ * n) * (minpoly R B.gen).coeff 0 ^ n) by
    have hndiv : ¬p ^ 2 ∣ (minpoly R B.gen).coeff 0 := fun h =>
      hei.notMem ((span_singleton_pow p 2).symm ▸ Ideal.mem_span_singleton.2 h)
    refine hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd (n := n) (?_ : _ ∣ _) hndiv
    convert! (IsUnit.dvd_mul_right ⟨(-1) ^ (n.succ * n), rfl⟩).mpr this using 1
    push_cast
    ring_nf
    simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
⊢ ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n

Tactic:
grind
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
⊢ ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n

Tactic:
have aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n := by grind
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
⊢ IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))

Tactic:
(hzint.mul (hBint.pow _)).sub (.sum _ fun i hi => .smul _ ?_)

Premises used: IsIntegral.mul, IsIntegral.sub, IsIntegral.pow, IsIntegral.smul, Polynomial.coeff, IsIntegral.sum
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
refine : ∀ (i : ℕ) (hi : i ∈ (range (Q.natDegree + 1)).erase 0), IsIntegral R (f (i + n))
⊢ IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))

Tactic:
refine (hzint.mul (hBint.pow _)).sub (.sum _ fun i hi => .smul _ ?_)

Premises used: IsIntegral.mul, IsIntegral.sub, IsIntegral.pow, IsIntegral.smul, IsIntegral.sum
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
i : ℕ
hi : i ∈ (range (Q.natDegree + 1)).erase 0
⊢ IsIntegral R (f (i + n))

Tactic:
adjoin_le_integralClosure hBint (hf _ (aux i hi)).1

Premises used: adjoin_le_integralClosure, Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, And.left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
i : ℕ
hi : i ∈ (range (Q.natDegree + 1)).erase 0
⊢ IsIntegral R (f (i + n))

Tactic:
exact adjoin_le_integralClosure hBint (hf _ (aux i hi)).1

Premises used: adjoin_le_integralClosure, And.left
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
⊢ IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))

Tactic:
have hintsum :
    IsIntegral R
      (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) := by
    refine (hzint.mul (hBint.pow _)).sub (.sum _ fun i hi => .smul _ ?_)
    exact adjoin_le_integralClosure hBint (hf _ (aux i hi)).1
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
obtain :
  ∀ (r : R)
    (hr :
      Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
        ((Algebra.norm K : (a : L) → K)
            (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) :
          K)),
    p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)
⊢ p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)

Tactic:
obtain ⟨r, hr⟩ := isIntegral_iff.1 (isIntegral_norm K hintsum)

Premises used: IsIntegrallyClosed.isIntegral_iff, Iff.mp, Algebra.isIntegral_norm
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
r : R
hr :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
    ((Algebra.norm K : (a : L) → K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) :
      K)
h : Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n) = p ^ n.succ * r
⊢ p ^ n.succ ∣ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)

Tactic:
use r
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
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
Q : R[X]
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hzint : IsIntegral R z
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
this : Module.Finite K L := ⋯
P : R[X] := minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
finrank_K_L : Module.finrank K L = B.dim
deg_K_P : natDegree (minpoly K B.gen) = B.dim
deg_R_P : P.natDegree = B.dim
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    B.dim ≤ i →
      Membership.mem (γ := Subalgebra R L) R[B.gen] (f i) ∧
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f i) = B.gen ^ i
aux : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, B.dim ≤ i + n
hintsum : IsIntegral R (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n))
r : R
hr :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
    ((Algebra.norm K : (a : L) → K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) :
      K)
h :
  Eq.{v + 1} (α := K)
    ((algebraMap R K : (a : R) → K)
        (Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n)) :
      K)
    ((algebraMap R K : (a : R) → K) (p ^ n.succ * r) : K)
⊢ Q.coeff 0 ^ n.succ * (HPow.hPow (α := R) (-1) (n.succ * n) * coeff (minpoly R B.gen) 0 ^ n) = p ^ n.succ * r

Tactic:
apply IsFractionRing.injective R K

Premises used: IsFractionRing.injective