-- 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
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
i : ℕ
neg : 0 ∈ range (Q.natDegree + 1) → p ∣ Q.coeff 0
neg₁ :
  ∀ (j : ℕ) (hind : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → p ∣ Q.coeff m),
    j + 1 ∈ range (Q.natDegree + 1) → p ∣ Q.coeff (j + 1)
⊢ i ∈ range (Q.natDegree + 1) → p ∣ Q.coeff i

Tactic:
induction i using Nat.case_strong_induction_on with
  | hz =>
    intro
    exact dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt hp hBint hQ hzint hei
  | hi j hind =>
    intro hj
    convert! hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd (n := n) _ hndiv
    -- Two technical results we will need about `P.natDegree` and `Q.natDegree`.
    have H := degree_modByMonic_lt Q₁ (minpoly.monic hBint)
    rw [← hQ₁, ← hP] at H
    replace H := Nat.lt_iff_add_one_le.1
      (lt_of_lt_of_le
        (lt_of_le_of_lt (Nat.lt_iff_add_one_le.1 (Nat.lt_of_succ_lt_succ (mem_range.1 hj)))
          (lt_succ_self _)) (Nat.lt_iff_add_one_le.1 ((natDegree_lt_natDegree_iff hQzero).2 H)))
    have Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j) := by
      rw [← add_comm 1, ← add_comm 1, add_assoc, add_right_inj,
        ← Nat.add_sub_assoc (Nat.lt_of_succ_lt_succ (mem_range.1 hj)).le, add_comm,
        Nat.add_sub_cancel]
    -- By induction hypothesis we can find `g : ℕ → R` such that
    -- `k ∈ range (j + 1) → Q.coeff k • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k`-
    choose! g hg using hind
    replace hg : ∀ k ∈ range (j + 1), Q.coeff k • B.gen ^ k =
        algebraMap R L p * g k • B.gen ^ k := by
      intro k hk
      rw [hg k (mem_range_succ_iff.1 hk)
        (mem_range_succ_iff.2
          (le_trans (mem_range_succ_iff.1 hk) (succ_le_iff.1 (mem_range_succ_iff.1 hj)).le)),
        Algebra.smul_def, Algebra.smul_def, map_mul, mul_assoc]
    -- Since `minpoly R B.gen` is Eisenstein, we can find `f : ℕ → L` such that
    -- `(map (algebraMap R L) (minpoly R B.gen)).nat_degree ≤ i` implies `f i ∈ R[B.gen]`
    -- and `(algebraMap R L) p * f i = B.gen ^ i`. We will also need `hf₁`, a reformulation of this
    -- property.
    choose! f hf using
      IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le (minpoly.aeval R B.gen)
        (minpoly.monic hBint) hei.isWeaklyEisensteinAt
    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
    -- The Eisenstein condition shows that `p` divides `Q.coeff j`
    -- if `p^n.succ` divides the following multiple of `Q.coeff (succ j)^n.succ`:
    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
    -- Using `hQ : aeval B.gen Q = p • z`, we write `p • z` as a sum of terms of degree less than
    -- `j+1`, that are multiples of `p` by induction, and terms of degree at least `j+1`.
    rw [aeval_eq_sum_range, Hj, range_add, sum_union (disjoint_range_addLeftEmbedding _ _),
      sum_congr rfl hg, add_comm] at hQ
    -- We multiply this equality by `B.gen ^ (P.natDegree-(j+2))`, so we can use `hf₁` on the terms
    -- we didn't know were multiples of `p`, and we take the norm on both sides.
    replace hQ := congr_arg (fun x => x * B.gen ^ (P.natDegree - (j + 2))) hQ
    simp_rw [sum_map, addLeftEmbedding_apply, add_mul, sum_mul, mul_assoc] at hQ
    rw [← insert_erase
      (mem_range.2 (tsub_pos_iff_lt.2 <| Nat.lt_of_succ_lt_succ <| mem_range.1 hj)),
      sum_insert (notMem_erase 0 _), add_zero, sum_congr rfl hf₁, ← mul_sum, ← mul_sum, add_assoc,
      ← mul_add, smul_mul_assoc, ← pow_add, Algebra.smul_def] at hQ
    replace hQ := congr_arg (norm K) (eq_sub_of_add_eq hQ)
    -- We obtain an equality of elements of `K`, but everything is integral, so we can move to `R`
    -- and simplify `hQ`.
    have hintsum : IsIntegral R (z * B.gen ^ (P.natDegree - (j + 2)) -
        (∑ 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)))) := by
      refine (hzint.mul (hBint.pow _)).sub
        (.add (.sum _ fun k hk => .smul _ ?_)
          (.sum _ fun k _ => .mul (.smul _ (.pow hBint _)) (hBint.pow _)))
      refine adjoin_le_integralClosure hBint (hf _ ?_).1
      rw [(minpoly.monic hBint).natDegree_map (algebraMap R L)]
      rw [add_comm, Nat.add_sub_assoc, le_add_iff_nonneg_right]
      · exact zero_le
      · refine one_le_iff_ne_zero.2 fun h => ?_
        rw [h] at hk
        simp at hk
    obtain ⟨r, hr⟩ := isIntegral_iff.1 (isIntegral_norm K hintsum)
    rw [Algebra.smul_def, mul_assoc, ← mul_sub, map_mul, algebraMap_apply R K L, map_pow,
      Algebra.norm_algebraMap, map_mul, algebraMap_apply R K L, Algebra.norm_algebraMap,
      finrank B, ← hr, PowerBasis.norm_gen_eq_coeff_zero_minpoly,
      minpoly.isIntegrallyClosed_eq_field_fractions' K hBint, coeff_map,
      show (-1 : K) = algebraMap R K (-1) by simp, ← map_pow, ← map_pow, ← map_mul, ←
      map_pow, ← map_mul, ← map_pow, ← map_mul] at hQ
    -- We can now finish the proof.
    have hppdiv : p ^ B.dim ∣ p ^ B.dim * r := dvd_mul_of_dvd_left dvd_rfl _
    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

Premises used: add_mul, Nat.case_strong_induction_on, Finset.mul_sum, Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, minpoly.monic, Polynomial.coeff_map, Nat.succ_eq_add_one, mul_sub, Units.coe_neg_one, IsFractionRing.injective, Finset.range_add, Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd, add_assoc, PowerBasis.finrank, mul_assoc, PowerBasis.gen, Finset.sum_map, pow_add, addLeftEmbedding_apply, smul_mul_assoc, Units.dvd_mul_left, Finset.sum_union, map_pow, minpoly.aeval, add_comm, Finset.disjoint_range_addLeftEmbedding, map_mul, Polynomial.IsEisensteinAt.isWeaklyEisensteinAt, Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le, dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt, Polynomial.aeval_eq_sum_range, mul_comm, Algebra.smul_def, mul_add, Finset.notMem_erase, Units.val_pow_eq_pow_val, Algebra.norm_algebraMap, Finset.sum_insert, add_zero, OfNat.ofNat, mul_pow, IsScalarTower.algebraMap_apply, Finset.sum_mul, minpoly.isIntegrallyClosed_eq_field_fractions'