-- Module: Mathlib.FieldTheory.SeparablyGenerated
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 : UniqueFactorizationMonoid.{u_2} ↥(Algebra.adjoin k (a '' {i}ᶜ))
coeff_ne :
  Ne (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
open open₁ open₂ :
  ∀
    (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))),
    IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)
open₃ :
  ∀
    (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)),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
open₄ :
  ∀
    (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),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
open₅ :
  ∀
    (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 (α := Polynomial ↥k') ((Polynomial.expand (↥k') p : (a : Polynomial ↥k') → Polynomial ↥k') g : Polynomial ↥k')
        (minpoly (↥k') (a i) : Polynomial ↥k')),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
open₆ :
  ∀
    (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))),
    Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
      (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
⊢ IsSeparable (↥(adjoin k (a '' {i}ᶜ))) (a i)

Tactic:
open scoped algebraAdjoinAdjoin in
  have hF₂irr := (hF₁irr.isPrimitive fun h ↦ coeff_ne <| Polynomial.coeff_eq_zero_of_natDegree_lt <|
    h.trans_lt <| Nat.pos_iff_ne_zero.2 hσi).irreducible_iff_irreducible_map_fraction_map
    (K := k').1 hF₁irr
  contrapose coeff_ne with Hsep
  have : CharP k' p := (expChar_of_injective_algebraMap (algebraMap k k').injective p).casesOn
    (fun e ↦ (e rfl).elim) (fun _ _ _ ↦ ‹_›) hp.ne_one
  obtain ⟨g, hg, eq⟩ := (((minpoly k' (a i)).separable_or p (minpoly.irreducible
    (isAlgebraic_iff_isIntegral.mp <| isAlgebraic_adjoin_iff.mpr alg))).resolve_left Hsep).2
  replace eq := congr(Polynomial.coeff $eq (σ i))
  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

Premises used: Polynomial.coeff_map, MulZeroClass.zero_mul, eq_mul_inv_iff_mul_eq₀, Nat.Prime.pos, Polynomial.coeff_mul_C, eq_comm, map_eq_zero_iff, FaithfulSMul.algebraMap_injective, Polynomial.coeff_expand, if_neg