-- 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
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
intro :
  ∀
    (H :
      Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0),
    False
intro₁ :
  ∀
    (H :
      Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0),
    False
refine_3 :
  ∀
    (H :
      Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0),
    let F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
      (optionEquivLeft k { b : ι // b ≠ i } :
          (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
        ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
            (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
          F);
    ∀
      (H :
        F.totalDegree ≤
          totalDegree.{u_1, u_3} (R := k) (σ := ι)
            ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) :
                (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
              (F₀.coeff ((σ : (a : ι) → ℕ) i)))),
      False
refine_1 :
  ∀
    (H :
      Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0),
    let F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
      (optionEquivLeft k { b : ι // b ≠ i } :
          (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
        ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
            (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
          F);
    Ne (α := MvPolynomial ι k)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
          (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
        MvPolynomial ι k)
      (0 : MvPolynomial ι k)
refine_2 :
  ∀
    (H :
      Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0),
    let F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
      (optionEquivLeft k { b : ι // b ≠ i } :
          (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
        ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
            (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
          F);
    Eq.{u_2 + 1} (α := K)
      ((aeval a : (a : MvPolynomial ι k) → K)
          ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) :
                (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
              (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
            MvPolynomial ι k) :
        K)
      (0 : K)
refine_1₁ :
  ∀
    (H :
      Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0),
    let F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
      (optionEquivLeft k { b : ι // b ≠ i } :
          (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
        ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
            (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
          F);
    Ne (α := MvPolynomial ι k)
      ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
          (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
        MvPolynomial ι k)
      (0 : MvPolynomial ι k)
refine_2₁ refine_2₂ :
  ∀
    (H :
      Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0),
    let F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
      (optionEquivLeft k { b : ι // b ≠ i } :
          (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
        ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
            (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
          F);
    Eq.{u_2 + 1} (α := K)
      ((aeval a : (a : MvPolynomial ι k) → K)
          ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) :
                (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
              (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
            MvPolynomial ι k) :
        K)
      (0 : K)
⊢ Ne (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0

Tactic:
classical
  intro H
  let F₀ := optionEquivLeft k _ (renameEquiv k (Equiv.optionSubtypeNe i).symm F)
  have H := HF (rename (↑) (F₀.coeff (σ i))) ?_ ?_
  · have : (F₀.coeff (σ i)).totalDegree + σ i ≤ _ :=
      totalDegree_coeff_optionEquivLeft_add_le _ _ _ (σ i) <| by
        rw [totalDegree_renameEquiv]
        exact (Finsupp.le_degree ..).trans (le_totalDegree hσ)
    rw [totalDegree_renameEquiv] at this
    simpa [hσi] using (this.trans H).trans (totalDegree_rename_le _ _)
  · refine (map_eq_zero_iff _ (rename_injective _ Subtype.val_injective)).not.mpr fun H ↦ ?_
    let e := (Equiv.optionSubtypeNe i).symm
    have : coeff _ (F₀.coeff _) = _ :=
      optionEquivLeft_coeff_some_coeff_none _ _ (σ.equivMapDomain e) (renameEquiv k e F)
    dsimp only [F₀] at this
    rw [renameEquiv_apply, Finsupp.equivMapDomain_eq_mapDomain, coeff_rename_mapDomain _
      e.injective, Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Equiv.optionSubtypeNe_none,
      ← renameEquiv_apply, H, coeff_zero, eq_comm, ← notMem_support_iff] at this
    exact this hσ
  · apply_fun Subalgebra.val _ at H
    simp_rw [toPolynomialAdjoinImageCompl, Polynomial.coe_mapAlgHom, Polynomial.coeff_map,
      AlgHom.coe_toRingHom, map_zero] at H
    simp_rw [← H, ← AlgHom.comp_apply]
    congr; ext; simp

Premises used: Iff.mpr, AlgHom.coe_toRingHom, Polynomial.coeff_map, MvPolynomial.notMem_support_iff, Subtype.val_injective, MvPolynomial.toPolynomialAdjoinImageCompl, Subalgebra.val, AlgHom.comp_apply, map_zero, Equiv.symm_symm, Iff.not, MvPolynomial.renameEquiv_apply, eq_comm, Finsupp.equivMapDomain_eq_mapDomain, MvPolynomial.totalDegree_renameEquiv, MvPolynomial.rename_injective, map_eq_zero_iff, MvPolynomial.coeff_zero, Finsupp.mapDomain_equiv_apply, Equiv.optionSubtypeNe_none, Polynomial.coe_mapAlgHom