-- 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 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:
rw [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective]

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_2
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 ^ r).natDegree < Fintype.card (L →ₐ[K] E)

Tactic:
rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]

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
σ : L →ₐ[K] E
⊢ ((σ x ^ r / σ ((aeval x) (derivative (minpoly K x)))) • map (↑σ) (minpolyDiv K x)).natDegree < finrank K L

Tactic:
exact ((Polynomial.natDegree_smul_le _ _).trans natDegree_map_le).trans_lt
  ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.isIntegral x)).trans_le
    (minpoly.natDegree_le _))

Result:
no goals

Proof state:
case hcard
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, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r).natDegree <
    Fintype.card (L →ₐ[K] E)

Tactic:
refine (Polynomial.natDegree_sub_le _ _).trans_lt
  (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_)

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
⊢ 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)

case hcard.refine_2
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 ^ r).natDegree < Fintype.card (L →ₐ[K] E)

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 = 0

Tactic:
have : Function.Injective (fun σ : L →ₐ[K] E ↦ σ x) := fun _ _ h =>
  AlgHom.ext_of_adjoin_eq_top hxL (fun _ hx ↦ hx ▸ h)

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
this : Function.Injective fun σ => σ x
⊢ ∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r = 0

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
⊢ ∀ (i : L →ₐ[K] E),
    eval (i x) (∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r) = 0

Tactic:
intro σ

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
⊢ eval (σ x) (∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv 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
this : Function.Injective fun σ => σ x
⊢ ∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r = 0

Tactic:
apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this

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
⊢ ∀ (i : L →ₐ[K] E),
    eval (i x) (∑ σ : L →ₐ[K] E, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r) = 0

case hcard
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, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) - X ^ r).natDegree <
    Fintype.card (L →ₐ[K] E)