awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
Goal:
R : Type u_2
S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
h : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree.{u_1} (R := S) 0 = natDegree.{u_2} (R := R) 0 - 1

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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 :
  ∑ σ : 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

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
⊢ 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)
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)
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)
⊢ ∑ σ : 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:
apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this

Premises used: Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
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
⊢ 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)

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]

Premises used: Finset.mem_univ, eval₂_minpolyDiv_self, Polynomial.eval_map, Finset.sum_ite_eq', RingHom.coe_coe, Polynomial.eval_X_pow, Function.Injective.eq_iff, mul_ite, ite_true, map_pow, Polynomial.eval_finsetSum, MulZeroClass.mul_zero, map_div₀, Polynomial.map_smul, Polynomial.eval_smul, smul_eq_mul, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
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)
⊢ 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:
rw [sub_eq_zero, div_mul_cancel₀]

Premises used: div_mul_cancel₀, sub_eq_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
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)
⊢ 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 [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective]

Premises used: ne_eq, RingHom.injective, AlgHom.toRingHom, map_eq_zero_iff
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L)
      (0 : L)

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

Premises used: Algebra.IsSeparable.isSeparable, minpoly.aeval, Polynomial.Separable.aeval_derivative_ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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_3 + 1} (α := L) ((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]) : L)
      (0 : L)

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

Premises used: Algebra.IsSeparable.isSeparable, Polynomial.Separable.aeval_derivative_ne_zero
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)

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

Premises used: Polynomial.natDegree_sum_le, max_lt, LE.le.trans_lt, Polynomial.natDegree_sub_le
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)
hcard₁ : (HPow.hPow (α := E[X]) X r).natDegree < 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)

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

Premises used: Polynomial.natDegree_sum_le, max_lt, LE.le.trans_lt, Polynomial.natDegree_sub_le
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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 :
  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
⊢ 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:
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]

Premises used: Finset.mem_univ, forall_true_left, RingHom.coe_coe, map_pow, map_div₀, AlgHom.card, Polynomial.map_smul, Finset.fold_max_lt, Function.comp_apply
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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

Tactic:
⟨finrank_pos, ?_⟩

Premises used: And.intro, Module.finrank_pos
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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 :
  ∀ (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
⊢ 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:
refine ⟨finrank_pos, ?_⟩
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
⊢ (HSMul.hSMul (β := E[X])
        (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))
        (map (↑σ : L →+* E) (minpolyDiv K x))).natDegree <
    finrank K L

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

Premises used: Algebra.IsIntegral.isIntegral, natDegree_minpolyDiv_lt, Polynomial.natDegree_smul_le, LT.lt.trans_le, Polynomial.natDegree_map_le, minpoly.natDegree_le, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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
⊢ (HSMul.hSMul (β := E[X])
        (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))
        (map (↑σ : L →+* E) (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 _))

Premises used: Algebra.IsIntegral.isIntegral, natDegree_minpolyDiv_lt, Polynomial.natDegree_smul_le, LT.lt.trans_le, Polynomial.natDegree_map_le, minpoly.natDegree_le, LE.le.trans, LE.le.trans_lt
-- Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv
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)
hcard₂ : r < Fintype.card (L →ₐ[K] E)
hcard₃ hcard₄ hcard₅ hcard₆ : r < finrank K L
⊢ (HPow.hPow (α := E[X]) X r).natDegree < Fintype.card (L →ₐ[K] E)

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

Premises used: Polynomial.natDegree_X, Polynomial.natDegree_pow, AlgHom.card, mul_one
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
obtain :
  ∀ (α : Eˣ) (hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x),
    ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤

Tactic:
obtain ⟨α, hα⟩ := @IsCyclic.exists_generator Eˣ _ _

Premises used: IsCyclic.exists_generator
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
h : Eq (α := IntermediateField F E) F⟮(↑α : E)⟯ ⊤
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤

Tactic:
use α
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
h : LE.le (α := IntermediateField F E) ⊤ F⟮(↑α : E)⟯
⊢ Eq (α := IntermediateField F E) F⟮(↑α : E)⟯ ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
pos : ∀ (hx : x = 0), Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
neg : ∀ (hx : ¬x = 0), Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : x = 0
pos : Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ 0
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x

Tactic:
rw [hx]
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : x = 0
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ 0

Tactic:
F⟮α.val⟯.zero_mem

Premises used: Units.val, IntermediateField.adjoin, IntermediateField.zero_mem, Singleton.singleton
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : x = 0
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ 0

Tactic:
exact F⟮α.val⟯.zero_mem

Premises used: Units.val, IntermediateField.adjoin, IntermediateField.zero_mem, Singleton.singleton
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : ¬x = 0
neg : ∀ (n : ℤ) (hn : α ^ n = Units.mk0 x hx), Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x

Tactic:
obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx))

Premises used: Set.mem_range, Units.mk0, Iff.mp
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
norm_cast : x = (↑(α ^ n) : E)
⊢ x = (↑α : E) ^ n

Tactic:
norm_cast
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
rw : x = (↑(Units.mk0 x hx : Eˣ) : E)
rw₁ rw₂ : x = x
⊢ x = (↑(α ^ n) : E)

Tactic:
rw [hn, Units.val_mk0]

Premises used: Units.val_mk0
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
neg : Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ ((↑α : E) ^ n)
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x

Tactic:
rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0]]
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ ((↑α : E) ^ n)

Tactic:
zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n

Premises used: Units.val, IntermediateField.mem_adjoin_simple_self, zpow_mem
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ ((↑α : E) ^ n)

Tactic:
exact zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n

Premises used: Units.val, IntermediateField.mem_adjoin_simple_self, zpow_mem
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite F
inst_4 : FiniteDimensional F E
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤

Tactic:
haveI : Finite E := Module.finite_of_finite F
  exists_primitive_element_of_finite_top F E

Premises used: Field.exists_primitive_element_of_finite_top