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 : 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)
i : ℕ
hi : i ∈ (range (Q.natDegree + 1)).erase 0
rw : Q.coeff i • B.gen ^ (i + n) = p • Q.coeff i • f (i + n)
rw₁ : Q.coeff i • HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (f (i + n)) = p • Q.coeff i • f (i + n)
rw₂ : Q.coeff i • p • f (i + n) = p • Q.coeff i • f (i + n)
rw₃ : (Q.coeff i * p) • f (i + n) = p • Q.coeff i • f (i + n)
rw₄ : (p * Q.coeff i) • f (i + n) = p • Q.coeff i • f (i + n)
rw₅ rw₆ : (p * Q.coeff i) • f (i + n) = (p * Q.coeff i) • f (i + n)
⊢ Q.coeff i • (B.gen ^ i * B.gen ^ n) = p • Q.coeff i • f (i + n)

Tactic:
rw [← pow_add, ← (hf _ (aux i hi)).2, ← Algebra.smul_def, smul_smul, mul_comm _ p, smul_smul]

Premises used: pow_add, smul_smul, And.right, mul_comm, Algebra.smul_def
-- 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)
⊢ ∀ i ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff i • (B.gen ^ i * B.gen ^ n) = p • Q.coeff i • f (i + n)

Tactic:
have : ∀ i ∈ (range (Q.natDegree + 1)).erase 0,
        Q.coeff i • (B.gen ^ i * B.gen ^ n) = p • Q.coeff i • f (i + n) := by
      intro i hi
      rw [← pow_add, ← (hf _ (aux i hi)).2, ← Algebra.smul_def, smul_smul, mul_comm _ p, smul_smul]
-- 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
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)
this : ∀ i ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff i • (B.gen ^ i * B.gen ^ n) = p • Q.coeff i • f (i + n)
⊢ Q.coeff 0 • B.gen ^ n + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n) =
    (HSMul.hSMul (β := L) (Q.coeff 0) 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n

Tactic:
simp only [add_mul, smul_mul_assoc, one_mul, sum_mul, sum_congr rfl this]

Premises used: add_mul, smul_mul_assoc, Finset.sum_congr, one_mul, rfl, Finset.sum_mul
-- 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 : 0 ∈ range (Q.natDegree + 1)
⊢ (Q.coeff 0 • HPow.hPow (β := ℕ) B.gen 0 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) *
      B.gen ^ n =
    HMul.hMul (α := L) ((aeval B.gen : (a : R[X]) → L) Q : L) (B.gen ^ n)

Tactic:
rw [aeval_eq_sum_range,
      Finset.add_sum_erase (range (Q.natDegree + 1)) fun i => Q.coeff i • B.gen ^ i]

Premises used: PowerBasis.gen, Polynomial.coeff, Finset.add_sum_erase, Finset.range, HPow.hPow, HAdd.hAdd, Polynomial.aeval_eq_sum_range, HSMul.hSMul, Polynomial.natDegree, OfNat.ofNat
-- 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)
⊢ 0 ∈ range (Q.natDegree + 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hQ : ∀ i ∈ range (Q.natDegree + 1), p ∣ Q.coeff i
hz : (aeval x : (a : A[X]) → B) Q = p • z
choose! :
  ∀ (f : (i : ℕ) → A) (hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i),
    Membership.mem (γ := Subalgebra A B) A[x] z
⊢ Membership.mem (γ := Subalgebra A B) A[x] z

Tactic:
choose! f hf using hQ
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : (aeval x : (a : A[X]) → B) Q = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
rw :
  ∀ (hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z) (f : (i : ℕ) → A)
    (hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i), Membership.mem (γ := Subalgebra A B) A[x] z
⊢ Membership.mem (γ := Subalgebra A B) A[x] z

Tactic:
rw [aeval_eq_sum_range, sum_range] at hz

Premises used: Finset.sum_range, Polynomial.aeval_eq_sum_range
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
congr : univ
f₁ : fun (i : Fin (Q.natDegree + 1)) ↦ Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ)
| ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ)

Tactic:
congr
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
| univ

Tactic:
next => skip
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
f₁ : ∀ (i : Fin (Q.natDegree + 1)), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ)
| fun (i : Fin (Q.natDegree + 1)) ↦ Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ)

Tactic:
ext i
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
i : Fin (Q.natDegree + 1)
f₁ : p • f (↑i : ℕ) • x ^ (↑i : ℕ)
| Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ)

Tactic:
rw [hf i (mem_range.2 (Fin.is_lt i)), ← smul_smul]

Premises used: Iff.mpr, smul_smul, Fin.is_lt, Finset.mem_range, Fin.val
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
f₁ : ∀ (i : Fin (Q.natDegree + 1)), p • f (↑i : ℕ) • x ^ (↑i : ℕ)
| ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ)

Tactic:
congr
    next => skip
    ext i
    rw [hf i (mem_range.2 (Fin.is_lt i)), ← smul_smul]

Premises used: smul_smul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
⊢ ∑ i : Fin (Q.natDegree + 1), p • f (↑i : ℕ) • x ^ (↑i : ℕ) = p • z

Tactic:
conv_lhs at hz =>
    congr
    next => skip
    ext i
    rw [hf i (mem_range.2 (Fin.is_lt i)), ← smul_smul]

Premises used: smul_smul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
hz : ∑ i : Fin (Q.natDegree + 1), Q.coeff (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
f : (i : ℕ) → A
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
hz₁ : ∑ i : Fin (Q.natDegree + 1), p • f (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
⊢ ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i

Tactic:
conv_lhs at hz =>
    congr
    next => skip
    ext i
    rw [hf i (mem_range.2 (Fin.is_lt i)), ← smul_smul]

Premises used: smul_smul
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
f : (i : ℕ) → A
hz : ∑ i : Fin (Q.natDegree + 1), p • f (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
⊢ HSMul.hSMul (β := B) p (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ)) = p • z

Tactic:
rw [← smul_sum] at hz

Premises used: Finset.smul_sum
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
f : (i : ℕ) → A
hz : ∑ i : Fin (Q.natDegree + 1), p • f (↑i : ℕ) • x ^ (↑i : ℕ) = p • z
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
hz₁ : HSMul.hSMul (β := B) p (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ)) = p • z
⊢ ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i

Tactic:
rw [← smul_sum] at hz

Premises used: Finset.smul_sum
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
f : (i : ℕ) → A
hz : HSMul.hSMul (β := B) p (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ)) = p • z
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
rw : Membership.mem (γ := Subalgebra A B) A[x] (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ))
⊢ Membership.mem (γ := Subalgebra A B) A[x] z

Tactic:
rw [← smul_right_injective _ hp hz]

Premises used: smul_right_injective
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
f : (i : ℕ) → A
hz : HSMul.hSMul (β := B) p (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ)) = p • z
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
⊢ Membership.mem (γ := Subalgebra A B) A[x] (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ))

Tactic:
Subalgebra.sum_mem _ fun _ _ =>
      Subalgebra.smul_mem _ (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _) _

Premises used: Set.mem_singleton, Algebra.subset_adjoin, Algebra.adjoin, Subalgebra.sum_mem, Fin.val, Subalgebra.smul_mem, Subalgebra.pow_mem, Singleton.singleton
-- Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : Ring B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : Module.IsTorsionFree A B
Q : A[X]
p : A
x z : B
hp : p ≠ 0
f : (i : ℕ) → A
hz : HSMul.hSMul (β := B) p (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ)) = p • z
hf : ∀ i ∈ range (Q.natDegree + 1), Q.coeff i = p * f i
⊢ Membership.mem (γ := Subalgebra A B) A[x] (∑ x_1 : Fin (Q.natDegree + 1), f (↑x_1 : ℕ) • x ^ (↑x_1 : ℕ))

Tactic:
exact
    Subalgebra.sum_mem _ fun _ _ =>
      Subalgebra.smul_mem _ (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton _)) _) _

Premises used: Set.mem_singleton, Algebra.subset_adjoin, Algebra.adjoin, Subalgebra.sum_mem, Subalgebra.smul_mem, Subalgebra.pow_mem, Singleton.singleton
-- 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
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
⊢ ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0

Tactic:
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)
-- 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
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
⊢ Module.Finite K L

Tactic:
have := B.finite
-- 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
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
this : Module.Finite K L
⊢ let P : R[X] := minpoly R B.gen;
  P.IsEisensteinAt (R ∙ p)

Tactic:
set P := minpoly R B.gen with hP

Premises used: PowerBasis.gen, minpoly
-- 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
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
this : Module.Finite K L
hei₁ :
  let P : R[X] := minpoly R B.gen;
  P.IsEisensteinAt (R ∙ p)
⊢ let P : R[X] := minpoly R B.gen;
  ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0

Tactic:
set P := minpoly R B.gen with hP

Premises used: PowerBasis.gen, minpoly
-- 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
hzint : IsIntegral R z
hz : Membership.mem (γ := Subalgebra R L) R[B.gen] (p • z)
hei : IsEisensteinAt (minpoly R B.gen) (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ coeff (minpoly R B.gen) 0
this : Module.Finite K L
hei₁ :
  let P : R[X] := minpoly R B.gen;
  P.IsEisensteinAt (R ∙ p)
hndiv₁ :
  let P : R[X] := minpoly R B.gen;
  ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
⊢ let P : R[X] := minpoly R B.gen;
  P = minpoly R B.gen

Tactic:
set P := minpoly R B.gen with hP

Premises used: PowerBasis.gen, minpoly
-- 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
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
obtain : ∀ (n : ℕ) (hn : B.dim = n.succ), Membership.mem (γ := Subalgebra R L) R[B.gen] z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z

Tactic:
obtain ⟨n, hn⟩ := Nat.exists_eq_succ_of_ne_zero B.dim_pos.ne'

Premises used: LT.lt.ne', PowerBasis.dim_pos, Nat.exists_eq_succ_of_ne_zero
-- 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
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
⊢ Module.IsTorsionFree R L

Tactic:
have : Module.IsTorsionFree R L := .trans_faithfulSMul R K L
-- 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
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
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
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen] z

Tactic:
rw [adjoin_singleton_eq_range_aeval] at hz

Premises used: Algebra.adjoin_singleton_eq_range_aeval