awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
⊢ natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ k + P.natDegree - 1
have rw : 0 ≤ k - 1
Tactic: rw [(minpoly.monic hBint).natDegree_map, add_comm, Nat.add_sub_assoc, le_add_iff_nonneg_right]
-- 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 : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
rw : 0 ≤ k - 1
⊢ natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ k + P.natDegree - 1
have h : 1 ≤ k
Tactic: rw [(minpoly.monic hBint).natDegree_map, add_comm, Nat.add_sub_assoc, le_add_iff_nonneg_right]
-- 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 : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
⊢ 1 ≤ k
have h : ∀ (h : k = 0), False
Tactic: refine one_le_iff_ne_zero.2 fun h => ?_
-- 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 : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
k : ℕ
hk : k ∈ (range (Q.natDegree - j)).erase 0
h : k = 0
⊢ False
have hk₁ : 0 ∈ (range (Q.natDegree - j)).erase 0
Tactic: rw [h] at hk
Cleared hypotheses: hk, h
-- 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 : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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 ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
have hf₁ : ∀ k ∈ (range (Q.natDegree - j)).erase 0,
  Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
    HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
Tactic: have hf₁ : ∀ k ∈ (range (Q.natDegree - j)).erase 0,
        Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
        (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1) := by
      intro k hk
      rw [smul_mul_assoc, ← pow_add, ← Nat.add_sub_assoc H, add_comm (j + 1) 1,
        add_assoc (j + 1), add_comm _ (k + P.natDegree), Nat.add_sub_add_right,
        ← (hf (k + P.natDegree - 1) _).2, mul_smul_comm]
      rw [(minpoly.monic hBint).natDegree_map, add_comm, Nat.add_sub_assoc, le_add_iff_nonneg_right]
      · exact Nat.zero_le _
      · refine one_le_iff_ne_zero.2 fun h => ?_
        rw [h] at hk
        simp at hk
-- 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
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
this : p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
have h : n = j.succ + (P.natDegree - (j + 2))
Tactic: convert! this
-- 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
hQ : (aeval B.gen : (a : R[X]) → L) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
this : p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
⊢ n = j.succ + (P.natDegree - (j + 2))
have h : j + 1 ≤ P.natDegree
Tactic: rw [Nat.succ_eq_add_one, add_assoc, ← Nat.add_sub_assoc H, add_comm (j + 1),
        Nat.add_sub_add_left, ← Nat.add_sub_assoc, Nat.add_sub_add_left, hP, ←
        (minpoly.monic hBint).natDegree_map (algebraMap R K), ←
        minpoly.isIntegrallyClosed_eq_field_fractions' K hBint, natDegree_minpoly, hn, Nat.sub_one,
        Nat.pred_succ]
-- 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 : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
⊢ p ^ n.succ ∣ Q.coeff (j + 1) ^ n.succ * P.coeff 0 ^ n
have neg : p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
Tactic: suffices
        p ^ n.succ ∣ Q.coeff (succ j) ^ n.succ *
          (minpoly R B.gen).coeff 0 ^ (succ j + (P.natDegree - (j + 2))) by
      convert! this
      rw [Nat.succ_eq_add_one, add_assoc, ← Nat.add_sub_assoc H, add_comm (j + 1),
        Nat.add_sub_add_left, ← Nat.add_sub_assoc, Nat.add_sub_add_left, hP, ←
        (minpoly.monic hBint).natDegree_map (algebraMap R K), ←
        minpoly.isIntegrallyClosed_eq_field_fractions' K hBint, natDegree_minpoly, hn, Nat.sub_one,
        Nat.pred_succ]
      lia
-- 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 : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
have neg : ∀ (hQzero : ¬Q = 0) (j : ℕ) (hj : j + 1 ∈ range (Q.natDegree + 1)) (H : j + 1 + 1 ≤ P.natDegree)
  (Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)) (g : (m : ℕ) → R)
  (hQ :
    HAdd.hAdd (α := L) (∑ x ∈ Finset.map (addLeftEmbedding (j + 1)) (range (Q.natDegree - j)), Q.coeff x • B.gen ^ x)
        (∑ x ∈ range (j + 1), HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g x • B.gen ^ x)) =
      p • z)
  (hg :
    ∀ k ∈ range (j + 1),
      Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k))
  (f : (i : ℕ) → L)
  (hf :
    ∀ (i : ℕ),
      natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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)
  (hf₁ :
    ∀ k ∈ (range (Q.natDegree - j)).erase 0,
      Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
        HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))),
  p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
Tactic: rw [aeval_eq_sum_range, Hj, range_add, sum_union (disjoint_range_addLeftEmbedding _ _),
      sum_congr rfl hg, add_comm] at hQ
Cleared hypotheses: hQ, hQzero, j, hj, H, Hj, g, hg, f, hf, hf₁
-- 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
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hQ :
  HAdd.hAdd (α := L) (∑ x ∈ Finset.map (addLeftEmbedding (j + 1)) (range (Q.natDegree - j)), Q.coeff x • B.gen ^ x)
      (∑ x ∈ range (j + 1), HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g x • B.gen ^ x)) =
    p • z
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
have hQ₂ : Eq.{z + 1} (α := L)
  ((fun (x : L) ↦ x * B.gen ^ (P.natDegree - (j + 2)))
    (HAdd.hAdd (α := L) (∑ x ∈ Finset.map (addLeftEmbedding (j + 1)) (range (Q.natDegree - j)), Q.coeff x • B.gen ^ x)
      (∑ x ∈ range (j + 1), HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g x • B.gen ^ x))))
  ((fun (x : L) ↦ x * B.gen ^ (P.natDegree - (j + 2))) (p • z))
Tactic: replace hQ := congr_arg (fun x => x * B.gen ^ (P.natDegree - (j + 2))) hQ
Cleared hypotheses: 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]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : (m : ℕ) → R
hg :
  ∀ k ∈ range (j + 1),
    Q.coeff k • B.gen ^ k = HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g k • B.gen ^ k)
f : (i : ℕ) → L
hf :
  ∀ (i : ℕ),
    natDegree (Polynomial.map (algebraMap R L) (minpoly R B.gen)) ≤ 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
hf₁ :
  ∀ k ∈ (range (Q.natDegree - j)).erase 0,
    Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (Q.coeff (j + 1 + k) • f (k + P.natDegree - 1))
hQ :
  Eq.{z + 1} (α := L)
    ((fun (x : L) ↦ x * B.gen ^ (P.natDegree - (j + 2)))
      (HAdd.hAdd (α := L) (∑ x ∈ Finset.map (addLeftEmbedding (j + 1)) (range (Q.natDegree - j)), Q.coeff x • B.gen ^ x)
        (∑ x ∈ range (j + 1), HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g x • B.gen ^ x))))
    ((fun (x : L) ↦ x * B.gen ^ (P.natDegree - (j + 2))) (p • z))
⊢ p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
have hQ₂ : HAdd.hAdd (α := L)
    (∑ i ∈ range (Q.natDegree - j), Q.coeff (j + 1 + i) • B.gen ^ (j + 1 + i) * B.gen ^ (P.natDegree - (j + 2)))
    (∑ x ∈ range (j + 1),
      HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L) (g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2)))) =
  p • z * B.gen ^ (P.natDegree - (j + 2))
Tactic: simp_rw [sum_map, addLeftEmbedding_apply, add_mul, sum_mul, mul_assoc] at hQ
Cleared hypotheses: hQ