-- 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
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 :
  (Algebra.norm K : (a : L) → K)
      (p • (z * B.gen ^ n) - HSMul.hSMul (β := L) p (∑ x ∈ (range (Q.natDegree + 1)).erase 0, 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)
h₁ :
  (Algebra.norm K : (a : L) → K)
      (p • (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, 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)
h₂ :
  (Algebra.norm K : (a : L) → K)
      (HMul.hMul (α := L) ((algebraMap R L : (a : R) → L) p : L)
        (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, 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)
h₃ :
  (Algebra.norm K : (a : L) → K)
      (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) ((algebraMap R K : (a : R) → K) p : K) : L)
        (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, 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)
h₄ :
  HMul.hMul (α := K) (β := K)
      ((Algebra.norm K : (a : L) → K) ((algebraMap K L : (a : K) → L) ((algebraMap R K : (a : R) → K) p : K) : L) : 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) =
    HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) p : K) n.succ)
      ((algebraMap R K : (a : R) → K) r : 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)
have h₅ : HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) p : K) (Module.finrank K L))
    ((Algebra.norm K : (a : L) → K) (z * B.gen ^ n - ∑ x ∈ (range (Q.natDegree + 1)).erase 0, Q.coeff x • f (x + n)) :
      K) =
  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: simp_rw [← smul_sum, ← smul_sub, Algebra.smul_def p, algebraMap_apply R K L, map_mul,
      Algebra.norm_algebraMap, finrank_K_L, hr, ← hn]