-- 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
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
⊢ Ne (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
have 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)
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