-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral (goal)
Goal:
R : Type u
K : Type v
L : Type z
p : R
inst : CommRing R
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
inst_7 : IsDomain R
inst_8 : IsFractionRing R K
inst_9 : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this_1 : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬HPow.hPow (β := ℕ) p 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
x : L[X] := Polynomial.map (algebraMap R L) P
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQzero : ¬Q = 0
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))
hintsum :
  IsIntegral R
    (z * B.gen ^ (P.natDegree - (j + 2)) -
      HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
        (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2))))
r : R
hQ :
  Eq.{v + 1} (α := K)
    ((algebraMap R K : (a : R) → K)
        (Q.coeff (j + 1) ^ B.dim *
          (HPow.hPow (α := R) (-1) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2)))) :
      K)
    ((algebraMap R K : (a : R) → K) (p ^ B.dim * r) : K)
hr :
  Eq.{v + 1} (α := K) ((algebraMap R K : (a : R) → K) r : K)
    ((Algebra.norm K : (a : L) → K)
        (z * B.gen ^ (P.natDegree - (j + 2)) -
          HAdd.hAdd (α := L) (∑ x ∈ (range (Q.natDegree - j)).erase 0, Q.coeff (j + 1 + x) • f (x + P.natDegree - 1))
            (∑ x ∈ range (j + 1), g x • B.gen ^ x * B.gen ^ (P.natDegree - (j + 2)))) :
      K)
hppdiv : p ^ B.dim ∣ p ^ B.dim * r
neg :
  ∀
    (hppdiv :
      p ^ B.dim ∣
        Q.coeff (j + 1) ^ B.dim *
          (HPow.hPow (α := R) (-1) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2)))),
    p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
neg₁ :
  ∀
    (hppdiv :
      p ^ B.dim ∣
        (HPow.hPow (α := R) (-1) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2))) *
          Q.coeff (j + 1) ^ B.dim),
    p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
neg₂ :
  ∀
    (hppdiv :
      p ^ B.dim ∣
        (HPow.hPow (α := R) (↑(-1) : R) B.dim * coeff (minpoly R B.gen) 0) ^ (j + 1 + (P.natDegree - (j + 2))) *
          Q.coeff (j + 1) ^ B.dim),
    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.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
have neg₃ : ∀
  (hppdiv :
    p ^ B.dim ∣
      HPow.hPow (α := R) (↑(-1) : R) B.dim ^ (j + 1 + (P.natDegree - (j + 2))) *
          coeff (minpoly R B.gen) 0 ^ (j + 1 + (P.natDegree - (j + 2))) *
        Q.coeff (j + 1) ^ B.dim),
  p ^ n.succ ∣ Q.coeff j.succ ^ n.succ * coeff (minpoly R B.gen) 0 ^ (j.succ + (P.natDegree - (j + 2)))
Tactic: rwa [← IsFractionRing.injective R K hQ, mul_comm, ← Units.coe_neg_one, mul_pow, ←
      Units.val_pow_eq_pow_val, ← Units.val_pow_eq_pow_val, mul_assoc,
      Units.dvd_mul_left, mul_comm, ← Nat.succ_eq_add_one, hn] at hppdiv
Cleared hypotheses: hppdiv