awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.MinpolyDiv (hypothesis)
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
⊢ ∑ σ : 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
have this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
Tactic: have : Function.Injective (fun σ : L →ₐ[K] E ↦ σ x) := fun _ _ h =>
    AlgHom.ext_of_adjoin_eq_top hxL (fun _ hx ↦ hx ▸ h)
-- 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
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
have heval : ∀ (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)
Tactic: apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
heval :
  ∀ (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 =
    0
have hcard : (∑ σ : 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: apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
σ : L →ₐ[K] E
⊢ Eq.{u_1 + 1} (α := E)
    (eval ((σ : (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)
have heval : HMul.hMul (β := E)
      (HDiv.hDiv (β := E) (HPow.hPow (α := E) ((σ : (a : L) → E) x : E) r)
        ((σ : (a : L) → E) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) :
          E))
      ((σ : (a : L) → E) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) : E) -
    HPow.hPow (α := E) ((σ : (a : L) → E) x : E) r =
  0
Tactic: 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]
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
σ : L →ₐ[K] E
⊢ HMul.hMul (β := E)
        (HDiv.hDiv (β := E) (HPow.hPow (α := E) ((σ : (a : L) → E) x : E) r)
          ((σ : (a : L) → E) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) :
            E))
        ((σ : (a : L) → E) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) :
          E) -
      HPow.hPow (α := E) ((σ : (a : L) → E) x : E) r =
    0
have heval : Ne.{u_1 + 1} (α := E)
  ((σ : (a : L) → E) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) : E)
  (0 : E)
Tactic: rw [sub_eq_zero, div_mul_cancel₀]
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
σ : L →ₐ[K] E
⊢ Ne.{u_1 + 1} (α := E)
    ((σ : (a : L) → E) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) : E)
    (0 : E)
have heval : ¬Eq.{u_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) (0 : L)
Tactic: rw [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective]
-- 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
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)
have hcard : Finset.fold (α := L →ₐ[K] E) max 0
    (Function.comp (β := E[X]) natDegree fun (σ : 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)))
    Finset.univ <
  Fintype.card (L →ₐ[K] E)
Tactic: refine (Polynomial.natDegree_sub_le _ _).trans_lt
      (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_)
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
hcard :
  Finset.fold (α := L →ₐ[K] E) max 0
      (Function.comp (β := E[X]) natDegree fun (σ : 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)))
      Finset.univ <
    Fintype.card (L →ₐ[K] 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).natDegree <
    Fintype.card (L →ₐ[K] E)
have hcard₁ : (HPow.hPow (α := E[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 ?_) ?_)
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
⊢ Finset.fold (α := L →ₐ[K] E) max 0
      (Function.comp (β := E[X]) natDegree fun (σ : 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)))
      Finset.univ <
    Fintype.card (L →ₐ[K] E)
have hcard : 0 < finrank K L ∧
  ∀ (x_1 : L →ₐ[K] E),
    (HSMul.hSMul (β := E[X])
          (HDiv.hDiv (β := E) (HPow.hPow (α := E) ((x_1 : (a : L) → E) x : E) r)
            ((x_1 : (a : L) → E)
                ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) :
              E))
          (map (↑x_1 : L →+* E) (minpolyDiv K x))).natDegree <
      finrank K L
Tactic: 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]
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
⊢ 0 < finrank K L ∧
    ∀ (x_1 : L →ₐ[K] E),
      (HSMul.hSMul (β := E[X])
            (HDiv.hDiv (β := E) (HPow.hPow (α := E) ((x_1 : (a : L) → E) x : E) r)
              ((x_1 : (a : L) → E)
                  ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) :
                E))
            (map (↑x_1 : L →+* E) (minpolyDiv K x))).natDegree <
        finrank K L
have hcard : ∀ (x_1 : L →ₐ[K] E),
  (HSMul.hSMul (β := E[X])
        (HDiv.hDiv (β := E) (HPow.hPow (α := E) ((x_1 : (a : L) → E) x : E) r)
          ((x_1 : (a : L) → E)
              ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L) :
            E))
        (map (↑x_1 : L →+* E) (minpolyDiv K x))).natDegree <
    finrank K L
Tactic: refine ⟨finrank_pos, ?_⟩
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
⊢ (HPow.hPow (α := E[X]) X r).natDegree < Fintype.card (L →ₐ[K] E)
have hcard : r * natDegree.{u_1} (R := E) X < Fintype.card (L →ₐ[K] E)
Tactic: rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
hcard : r * natDegree.{u_1} (R := E) X < Fintype.card (L →ₐ[K] E)
⊢ (HPow.hPow (α := E[X]) X r).natDegree < Fintype.card (L →ₐ[K] E)
have hcard₁ : r * 1 < Fintype.card (L →ₐ[K] E)
Tactic: rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]
-- 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
this : Function.Injective (β := E) fun (σ : L →ₐ[K] E) ↦ (σ : (a : L) → E) x
hcard : r * natDegree.{u_1} (R := E) X < Fintype.card (L →ₐ[K] E)
hcard₁ : r * 1 < Fintype.card (L →ₐ[K] E)
⊢ (HPow.hPow (α := E[X]) X r).natDegree < Fintype.card (L →ₐ[K] E)
have hcard₂ : r < Fintype.card (L →ₐ[K] E)
Tactic: rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]
-- 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
⊢ ∑ σ : 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 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
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]
-- 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
⊢ ∑ σ : 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 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
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]
-- 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
⊢ ∑ σ : 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 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
have obtain : ∀ (α : Eˣ) (hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x),
  ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
Tactic: obtain ⟨α, hα⟩ := @IsCyclic.exists_generator Eˣ _ _
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
have h : Eq (α := IntermediateField F E) F⟮(↑α : E)⟯ ⊤
Tactic: use α
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
⊢ Eq (α := IntermediateField F E) F⟮(↑α : E)⟯ ⊤
have h : LE.le (α := IntermediateField F E) ⊤ F⟮(↑α : E)⟯
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
have pos : ∀ (hx : x = 0), Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
Tactic: by_cases hx : x = 0