-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (goal)
Goal:
K : Type u_2
L : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_1
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hxL : Eq (α := Subalgebra K L) K[x] ⊤
r : ℕ
hr : r < finrank K L
rw rw₁ rw₂ :
  ∑ σ : L →ₐ[K] E,
        map (↑σ : L →+* E)
          (HSMul.hSMul (β := L[X])
            (HDiv.hDiv (β := L) (x ^ r)
              ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L))
            (minpolyDiv K x)) -
      HPow.hPow (α := E[X]) X r =
    0
rw₃ :
  ∀ (this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x),
    ∑ σ : L →ₐ[K] E,
          map (↑σ : L →+* E)
            (HSMul.hSMul (β := L[X])
              (HDiv.hDiv (β := L) (x ^ r)
                ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L))
              (minpolyDiv K x)) -
        HPow.hPow (α := E[X]) X r =
      0
heval :
  ∀ (this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x) (i : L →ₐ[K] E),
    Eq.{u_1 + 1} (α := E)
      (eval ((i : (a : L) → E) x)
          (∑ σ : L →ₐ[K] E,
              map (↑σ : L →+* E)
                (HSMul.hSMul (β := L[X])
                  (HDiv.hDiv (β := L) (x ^ r)
                    ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L))
                  (minpolyDiv K x)) -
            HPow.hPow (α := E[X]) X r) :
        E)
      (0 : E)
⊢ ∑ σ : L →ₐ[K] E,
      map (↑σ : L →+* E)
        (HSMul.hSMul (β := L[X])
          (HDiv.hDiv (β := L) (x ^ r)
            ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L))
          (minpolyDiv K x)) =
    HPow.hPow (α := E[X]) X r
have hcard : ∀ (this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x),
  (∑ σ : L →ₐ[K] E,
          map (↑σ : L →+* E)
            (HSMul.hSMul (β := L[X])
              (HDiv.hDiv (β := L) (x ^ r)
                ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L))
              (minpolyDiv K x)) -
        HPow.hPow (α := E[X]) X r).natDegree <
    Fintype.card (L →ₐ[K] E)
Tactic: classical
  rw [← sub_eq_zero]
  have : Function.Injective (fun σ : L →ₐ[K] E ↦ σ x) := fun _ _ h =>
    AlgHom.ext_of_adjoin_eq_top hxL (fun _ hx ↦ hx ▸ h)
  apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this
  · intro σ
    simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, eval_sub, eval_finsetSum,
      eval_smul, eval_map, eval₂_minpolyDiv_self, this.eq_iff, smul_eq_mul, mul_ite, mul_zero,
      Finset.sum_ite_eq', Finset.mem_univ, ite_true, eval_X_pow]
    rw [sub_eq_zero, div_mul_cancel₀]
    rw [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective]
    exact (IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
  · refine (Polynomial.natDegree_sub_le _ _).trans_lt
      (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_)
    · simp only [Polynomial.map_smul,
        map_div₀, map_pow, RingHom.coe_coe, Function.comp_apply,
        Finset.mem_univ, forall_true_left, Finset.fold_max_lt, AlgHom.card]
      refine ⟨finrank_pos, ?_⟩
      intro σ
      exact ((Polynomial.natDegree_smul_le _ _).trans natDegree_map_le).trans_lt
        ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.isIntegral x)).trans_le
          (minpoly.natDegree_le _))
    · rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]