-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma sum_smul_minpolyDiv_eq_X_pow (E) [Field E] [Algebra K E] [IsAlgClosed E]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    {x : L} (hxL : Algebra.adjoin K {x} = ⊤) {r : ℕ} (hr : r < finrank K L) :
    ∑ σ : L →ₐ[K] E, ((x ^ r / aeval x (derivative <| minpoly K x)) •
      minpolyDiv K x).map σ = (X ^ r : E[X])

Proof state:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
⊢ 0 < finrank K L ∧
    ∀ (x_1 : L →ₐ[K] E),
      ((x_1 x ^ r / x_1 ((aeval x) (derivative (minpoly K x)))) • map (↑x_1) (minpolyDiv K x)).natDegree < finrank K L

Tactic:
refine ⟨finrank_pos, ?_⟩

Result:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
⊢ ∀ (x_1 : L →ₐ[K] E),
    ((x_1 x ^ r / x_1 ((aeval x) (derivative (minpoly K x)))) • map (↑x_1) (minpolyDiv K x)).natDegree < finrank K L

Proof state:
case heval.h
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
σ : L →ₐ[K] E
⊢ ¬(aeval x) (derivative (minpoly K x)) = 0

Tactic:
exact (Algebra.IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)

Result:
no goals

Proof state:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
⊢ ∀ (x_1 : L →ₐ[K] E),
    ((x_1 x ^ r / x_1 ((aeval x) (derivative (minpoly K x)))) • map (↑x_1) (minpolyDiv K x)).natDegree < finrank K L

Tactic:
intro σ

Result:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
σ : L →ₐ[K] E
⊢ ((σ x ^ r / σ ((aeval x) (derivative (minpoly K x)))) • map (↑σ) (minpolyDiv K x)).natDegree < finrank K L

Proof state:
case heval
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
σ : L →ₐ[K] E
⊢ σ x ^ r / σ ((aeval x) (derivative (minpoly K x))) * σ ((aeval x) (derivative (minpoly K x))) - σ x ^ r = 0

Tactic:
rw [sub_eq_zero, div_mul_cancel₀]

Result:
case heval.h
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
σ : L →ₐ[K] E
⊢ σ ((aeval x) (derivative (minpoly K x))) ≠ 0

Proof state:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
⊢ Finset.fold max 0 (natDegree ∘ fun σ => map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x))
      Finset.univ <
    Fintype.card (L →ₐ[K] E)

Tactic:
simp only [AlgEquiv.toAlgHom_eq_coe, Polynomial.map_smul,
  map_div₀, map_pow, RingHom.coe_coe, AlgHom.coe_coe, Function.comp_apply,
  Finset.mem_univ, forall_true_left, true_and, Finset.fold_max_lt, AlgHom.card]

Result:
case hcard.refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
⊢ 0 < finrank K L ∧
    ∀ (x_1 : L →ₐ[K] E),
      ((x_1 x ^ r / x_1 ((aeval x) (derivative (minpoly K x)))) • map (↑x_1) (minpolyDiv K x)).natDegree < finrank K L

Proof state:
case heval
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
σ : L →ₐ[K] E
⊢ eval (σ x) (∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r) = 0

Tactic:
simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, eval_sub, eval_finset_sum,
  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_pow, eval_X]

Result:
case heval
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
this : Function.Injective fun σ => σ x
σ : L →ₐ[K] E
⊢ σ x ^ r / σ ((aeval x) (derivative (minpoly K x))) * σ ((aeval x) (derivative (minpoly K x))) - σ x ^ r = 0

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) = X ^ r

Tactic:
rw [← sub_eq_zero]

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : Algebra.adjoin K {x} = ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r = 0