-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id (↑s : Set K) → LinearIndepOn k (M := K) (fun (x : K) ↦ x ^ p) (↑s : Set K)
a : ι → K
n : ι
inst_3 : ExpChar k p
ha' : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (i : { i : ι // i ≠ n }) ↦ a (↑i : ι)
S : Set (MvPolynomial ι k) :=
  {F : MvPolynomial ι k | F ≠ 0 ∧ Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)}
F : MvPolynomial ι k
hFmin :
  ∀ (G : MvPolynomial ι k),
    G ≠ 0 → Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) G : K) (0 : K) → F.totalDegree ≤ G.totalDegree
hF₀ : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
hFirr : Irreducible F
i : ι
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hi : ¬p ∣ (σ : (a : ι) → ℕ) i
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
alg : IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)
Hi : IsTranscendenceBasis.{u_3, u_1, u_2} k (A := K) fun (x : { x : ι // x ≠ i }) ↦ a (↑x : ι)
k' : IntermediateField k K := adjoin k (a '' {i}ᶜ)
hF₁irr : Irreducible (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i)
this_1 : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
hF₂irr :
  Irreducible (M := Polynomial ↥k')
    (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
      (F.toPolynomialAdjoinImageCompl a i))
Hsep : ¬IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
this : CharP.{u_2} (↥k') p
g : Polynomial ↥k'
hg : Irreducible g
eq :
  Eq (α := ↥k')
    (Polynomial.coeff ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g) ((σ : (a : ι) → ℕ) i))
    (Polynomial.coeff (minpoly (↥k') (a i)) ((σ : (a : ι) → ℕ) i))
rwa :
  ∀
    (eq :
      Polynomial.coeff ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g) ((σ : (a : ι) → ℕ) i) =
        (HMul.hMul (α := Polynomial ↥k')
              (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
                (F.toPolynomialAdjoinImageCompl a i))
              ((Polynomial.C : (a : ↥k') → Polynomial ↥k')
                (Polynomial.leadingCoeff
                    (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
                      (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k') (F.toPolynomialAdjoinImageCompl a i)))⁻¹)).coeff
          ((σ : (a : ι) → ℕ) i)),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
rwa₁ :
  ∀
    (eq :
      Polynomial.coeff ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g) ((σ : (a : ι) → ℕ) i) =
        HMul.hMul (α := ↥k')
          (Polynomial.coeff
            (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
              (F.toPolynomialAdjoinImageCompl a i))
            ((σ : (a : ι) → ℕ) i))
          (Polynomial.leadingCoeff
              (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
                (F.toPolynomialAdjoinImageCompl a i)))⁻¹),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
rwa₂ :
  ∀
    (eq :
      (if p ∣ (σ : (a : ι) → ℕ) i then g.coeff (HDiv.hDiv (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) p) else 0) =
        HMul.hMul (α := ↥k')
          (Polynomial.coeff
            (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
              (F.toPolynomialAdjoinImageCompl a i))
            ((σ : (a : ι) → ℕ) i))
          (Polynomial.leadingCoeff
              (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
                (F.toPolynomialAdjoinImageCompl a i)))⁻¹),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
rwa₃ :
  ∀
    (eq :
      0 =
        HMul.hMul (α := ↥k')
          (Polynomial.coeff
            (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
              (F.toPolynomialAdjoinImageCompl a i))
            ((σ : (a : ι) → ℕ) i))
          (Polynomial.leadingCoeff
              (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
                (F.toPolynomialAdjoinImageCompl a i)))⁻¹),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
⊢ Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
have rwa₄ : ∀
  (eq :
    HMul.hMul (α := ↥k') 0
        (Polynomial.leadingCoeff
          (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
            (F.toPolynomialAdjoinImageCompl a i))) =
      Polynomial.coeff
        (Polynomial.map (R := ↥(Algebra.adjoin k (a '' {i}ᶜ))) (algebraMap ↥(Algebra.adjoin k (a '' {i}ᶜ)) ↥k')
          (F.toPolynomialAdjoinImageCompl a i))
        ((σ : (a : ι) → ℕ) i)),
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
Tactic: rwa [← minpoly.eq_of_irreducible hF₂irr ((Polynomial.aeval_map_algebraMap ..).trans
    (aeval_toPolynomialAdjoinImageCompl_eq_zero hFa i)), Polynomial.coeff_mul_C,
    Polynomial.coeff_expand hp.pos, if_neg hi, eq_mul_inv_iff_mul_eq₀
    (by simpa using hF₂irr.ne_zero), zero_mul, eq_comm,
    Polynomial.coeff_map, map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ..)] at eq
Cleared hypotheses: eq