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)
h :
  HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) n.succ *
      (HPow.hPow (α := K) (-1) (n.succ * n) *
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) n) =
    HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) p : K) n.succ)
      ((algebraMap R K : (a : R) → K) r : K)
⊢ 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)

Tactic:
simp only [map_mul, map_pow, map_neg, map_one]

Premises used: map_neg, map_pow, map_mul, map_one
-- 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)
⊢ HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) n.succ *
      (HPow.hPow (α := K) (-1) (n.succ * n) *
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) n) =
    (Algebra.norm K : (a : L) → K) (Q.coeff 0 • B.gen ^ n)

Tactic:
?_
-- 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)
⊢ Eq.{v + 1} (α := K) ((Algebra.norm K : (a : L) → K) (Q.coeff 0 • B.gen ^ n) : K)
    ((Algebra.norm K : (a : L) → K)
        (p • (z * B.gen ^ n) - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n)) :
      K)

Tactic:
(congr_arg (norm K) (eq_sub_of_add_eq ?_))

Premises used: eq_sub_of_add_eq, congr_arg, Algebra.norm, DFunLike.coe
-- 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)
⊢ (Algebra.norm K : (a : L) → K)
      (p • (z * B.gen ^ n) - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n)) =
    HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) p : K) n.succ)
      ((algebraMap R K : (a : R) → K) r : K)

Tactic:
?_
-- 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 :
  HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) n.succ *
      (HPow.hPow (α := K) (-1) (n.succ * n) *
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) n) =
    (Algebra.norm K : (a : L) → K) (Q.coeff 0 • B.gen ^ n)
h₁ : Q.coeff 0 • B.gen ^ n + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n) = p • (z * B.gen ^ n)
h₂ :
  (Algebra.norm K : (a : L) → K)
      (p • (z * B.gen ^ n) - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n)) =
    HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) p : K) n.succ)
      ((algebraMap R K : (a : R) → K) r : K)
⊢ HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) n.succ *
      (HPow.hPow (α := K) (-1) (n.succ * n) *
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) n) =
    HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) p : K) n.succ)
      ((algebraMap R K : (a : R) → K) r : K)

Tactic:
calc
    _ = norm K (Q.coeff 0 • B.gen ^ n) := ?_
    _ = norm K (p • (z * B.gen ^ n) -
          ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n)) :=
        (congr_arg (norm K) (eq_sub_of_add_eq ?_))
    _ = _ := ?_

Premises used: HMul.hMul, eq_sub_of_add_eq, PowerBasis.gen, HSub.hSub, Polynomial.coeff, congr_arg, Finset.range, HPow.hPow, HAdd.hAdd, HSMul.hSMul, Polynomial.natDegree, Algebra.norm, OfNat.ofNat, Finset.erase, DFunLike.coe, Finset.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
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 :
  HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) B.dim *
      (HPow.hPow (α := K) (-1) (B.dim * n) *
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) n) =
    HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) B.dim *
      HMul.hMul (β := K) (HPow.hPow (α := K) (-1) B.dim)
          ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) ^
        n
⊢ HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) n.succ *
      (HPow.hPow (α := K) (-1) (n.succ * n) *
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) n) =
    (Algebra.norm K : (a : L) → K) (Q.coeff 0 • B.gen ^ n)

Tactic:
simp only [Algebra.smul_def, algebraMap_apply R K L, Algebra.norm_algebraMap, map_mul,
      map_pow, finrank_K_L, PowerBasis.norm_gen_eq_coeff_zero_minpoly,
      minpoly.isIntegrallyClosed_eq_field_fractions' K hBint, coeff_map, ← hn]

Premises used: Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, Polynomial.coeff_map, map_pow, map_mul, Algebra.smul_def, Algebra.norm_algebraMap, IsScalarTower.algebraMap_apply, minpoly.isIntegrallyClosed_eq_field_fractions'
-- 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)
⊢ HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) B.dim *
      (HPow.hPow (α := K) (-1) (B.dim * n) *
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) n) =
    HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) (Q.coeff 0) : K) B.dim *
      HMul.hMul (β := K) (HPow.hPow (α := K) (-1) B.dim)
          ((algebraMap R K : (a : R) → K) (coeff (minpoly R B.gen) 0) : K) ^
        n

Tactic:
ring
-- 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)
⊢ 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:
?_
-- 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)
rw rw₁ :
  (HSMul.hSMul (β := L) (Q.coeff 0) 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n =
    (HSMul.hSMul (β := L) (Q.coeff 0) 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n
⊢ (HSMul.hSMul (β := L) (Q.coeff 0) 1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n =
    (Q.coeff 0 • HPow.hPow (β := ℕ) B.gen 0 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) *
      B.gen ^ n

Tactic:
rw [pow_zero]

Premises used: pow_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
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)
⊢ (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:
?_
-- 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)
rw : p • z * B.gen ^ n = p • (z * B.gen ^ n)
rw₁ rw₂ : p • (z * B.gen ^ n) = p • (z * B.gen ^ n)
⊢ HMul.hMul (α := L) ((aeval B.gen : (a : R[X]) → L) Q : L) (B.gen ^ n) = p • (z * B.gen ^ n)

Tactic:
rw [hQ, Algebra.smul_mul_assoc]

Premises used: Algebra.smul_mul_assoc
-- 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 • 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
h₁ :
  (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)
⊢ Q.coeff 0 • B.gen ^ n + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, p • Q.coeff x • f (x + n) = p • (z * B.gen ^ n)

Tactic:
calc
    _ = (Q.coeff 0 • ↑1 + ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) *
          B.gen ^ n := ?_
    _ = (Q.coeff 0 • B.gen ^ 0 +
        ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • B.gen ^ x) * B.gen ^ n := by
      rw [pow_zero]
    _ = aeval B.gen Q * B.gen ^ n := ?_
    _ = _ := by rw [hQ, Algebra.smul_mul_assoc]

Premises used: PowerBasis.gen, Polynomial.coeff, Finset.range, HPow.hPow, HAdd.hAdd, HSMul.hSMul, Polynomial.aeval, Polynomial.natDegree, OfNat.ofNat, Finset.erase, DFunLike.coe, Finset.sum