awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
hn : 0 < n
hndvd : ¬n ∣ n * s.natDegree + m
⊢ s.leadingCoeff ≠ 0

Tactic:
leadingCoeff_ne_zero.2 hzero

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
hn : 0 < n
hndvd : ¬n ∣ n * s.natDegree + m
⊢ s.leadingCoeff ≠ 0

Tactic:
exact leadingCoeff_ne_zero.2 hzero

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
⊢ f.coeff (n * s.natDegree + m) ≠ 0

Tactic:
have : f.coeff (n * s.natDegree + m) ≠ 0 := by
      have hn : 0 < n := by linarith only [hm, hmn]
      have hndvd : ¬ n ∣ n * s.natDegree + m := by
        rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)]
        exact Nat.not_dvd_of_pos_of_lt hm hmn
      simp only [f, coeff_sub, coeff_X_pow_mul, s.coeff_expand_mul' hn, coeff_natDegree,
        coeff_expand hn r, hndvd, ite_false, sub_zero]
      exact leadingCoeff_ne_zero.2 hzero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h_1 :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
this : f.coeff (n * s.natDegree + m) ≠ 0
h : f = 0
⊢ False

Tactic:
simp only [h, coeff_zero, ne_eq, not_true_eq_false] at this

Premises used: not_true_eq_false, ne_eq, Polynomial.coeff_zero
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F_1 : Type u_1
E_1 : Type u_2
inst : Field F_1
inst_1 : Field E_1
inst_2 : Algebra F_1 E_1
F : Type u_1
E : Type u_2
inst_3 : Field F
inst_4 : Field E
inst_5 : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : Eq (α := IntermediateField F E) F⟮α ^ m⟯ F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h :
  HSub.hSub (β := E) (HMul.hMul (β := E) (α ^ m) ((aeval (α ^ n) : (a : F[X]) → E) s : E))
      ((aeval (α ^ n) : (a : F[X]) → E) r : E) =
    0
hm : 0 < m
hzero : s ≠ 0
f : F[X] :=
  HSub.hSub (β := F[X]) (HMul.hMul (β := F[X]) (HPow.hPow (α := F[X]) X m) ((expand F n : (a : F[X]) → F[X]) s : F[X]))
    ((expand F n : (a : F[X]) → F[X]) r : F[X])
⊢ Eq.{u_2 + 1} (α := E) ((aeval α : (a : F[X]) → E) f : E) (0 : E)

Tactic:
simp only [f, map_sub, map_mul, map_pow, aeval_X, expand_aeval, h]

Premises used: map_sub, map_pow, map_mul, Polynomial.expand_aeval, Polynomial.aeval_X
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
⊢ Algebra.IsAlgebraic F E

Tactic:
⟨fun α ↦
  have ⟨_m, _n, hneq, heq⟩ := Finite.exists_ne_map_eq_of_infinite fun n ↦ F⟮α ^ n⟯
  isAlgebraic_of_adjoin_eq_adjoin F E hneq heq⟩

Premises used: IsAlgebraic, _private.0.Field.isAlgebraic_of_finite_intermediateField.match_1, Algebra.IsAlgebraic.mk, Field.isAlgebraic_of_adjoin_eq_adjoin, Finite.exists_ne_map_eq_of_infinite, HPow.hPow, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
⊢ Algebra.IsAlgebraic F E

Tactic:
have := isAlgebraic_of_finite_intermediateField F E
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
this : Algebra.IsAlgebraic F E
⊢ ∀ (K : IF), FiniteDimensional.{u_1, u_2} F ↥(↑K : IntermediateField F E)

Tactic:
haveI : ∀ K : IF, FiniteDimensional F K.1 := fun ⟨_, x, rfl⟩ ↦ adjoin.finiteDimensional
    (Algebra.IsIntegral.isIntegral _)
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
this_1 : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional.{u_1, u_2} F ↥(↑K : IntermediateField F E)
⊢ FiniteDimensional.{u_1, u_2} F ↥(⨆ (i : IF), (↑i : IntermediateField F E))

Tactic:
have hfin := finiteDimensional_iSup_of_finite (t := fun K : IF ↦ K.1)
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
this_1 : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional.{u_1, u_2} F ↥(↑K : IntermediateField F E)
hfin : FiniteDimensional.{u_1, u_2} F ↥(⨆ (i : IF), (↑i : IntermediateField F E))
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (K : IF), (↑K : IntermediateField F E)) ⊤

Tactic:
have htop : ⨆ K : IF, K.1 = ⊤ := le_top.antisymm fun x _ ↦
    le_iSup (fun K : IF ↦ K.1) ⟨F⟮x⟯, x, rfl⟩ <| mem_adjoin_simple_self F x
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
this_1 : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional.{u_1, u_2} F ↥(↑K : IntermediateField F E)
hfin : FiniteDimensional.{u_1, u_2} F ↥(⨆ (i : IF), (↑i : IntermediateField F E))
htop : Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (K : IF), (↑K : IntermediateField F E)) ⊤
⊢ FiniteDimensional.{u_1, u_2} F ↥⊤

Tactic:
rw [htop] at hfin
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
this_1 : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional.{u_1, u_2} F ↥(↑K : IntermediateField F E)
hfin : FiniteDimensional.{u_1, u_2} F ↥(⨆ (i : IF), (↑i : IntermediateField F E))
htop : Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (K : IF), (↑K : IntermediateField F E)) ⊤
hfin₁ : FiniteDimensional.{u_1, u_2} F ↥⊤
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (K : IF), (↑K : IntermediateField F E)) ⊤

Tactic:
rw [htop] at hfin
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
this_1 : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional.{u_1, u_2} F ↥(↑K : IntermediateField F E)
hfin : FiniteDimensional.{u_1, u_2} F ↥⊤
htop : Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (K : IF), (↑K : IntermediateField F E)) ⊤
⊢ FiniteDimensional F E

Tactic:
topEquiv.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
IF : Type (max 0 u_2) := { K : IntermediateField F E // ∃ (x : E), K = F⟮x⟯ }
this_1 : Algebra.IsAlgebraic F E
this : ∀ (K : IF), FiniteDimensional.{u_1, u_2} F ↥(↑K : IntermediateField F E)
hfin : FiniteDimensional.{u_1, u_2} F ↥⊤
htop : Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (K : IF), (↑K : IntermediateField F E)) ⊤
⊢ FiniteDimensional F E

Tactic:
exact topEquiv.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
⊢ FiniteDimensional F E

Tactic:
haveI := FiniteDimensional.of_finite_intermediateField F E
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
inl : Finite F → ∃ (α : E), F⟮α⟯ = K
inr : Infinite F → ∃ (α : E), F⟮α⟯ = K
⊢ ∃ (α : E), F⟮α⟯ = K

Tactic:
rcases finite_or_infinite F with (_ | _)

Premises used: finite_or_infinite
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h : Finite F
inl : ∀ (α : ↥K) (h : Eq (α := IntermediateField F ↥K) F⟮α⟯ ⊤), ∃ (α : E), F⟮α⟯ = K
⊢ ∃ (α : E), F⟮α⟯ = K

Tactic:
obtain ⟨α, h⟩ := exists_primitive_element_of_finite_bot F K

Premises used: Membership.mem, Field.exists_primitive_element_of_finite_bot, Subtype
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h_1 : Finite F
α : ↥K
h : Eq (α := IntermediateField F ↥K) F⟮α⟯ ⊤
⊢ F⟮(↑α : E)⟯ = K

Tactic:
simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h

Premises used: IntermediateField.lift, IntermediateField.lift_adjoin_simple, IntermediateField.lift_top, congr_arg
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h_1 : Finite F
α : ↥K
h : Eq (α := IntermediateField F ↥K) F⟮α⟯ ⊤
⊢ ∃ (α : E), F⟮α⟯ = K

Tactic:
exact ⟨α, by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h⟩
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h : Infinite F
inr :
  ∀ (K : IntermediateField F E) (x : E),
    (∃ (α : E), F⟮α⟯ = K) →
      ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ ∃ (α : E), F⟮α⟯ = K

Tactic:
apply induction_on_adjoin (fun K ↦ ∃ α : E, F⟮α⟯ = K) ⟨0, adjoin_zero⟩

Premises used: IntermediateField.adjoin_zero, Exists, IntermediateField.adjoin, Exists.intro, Singleton.singleton, OfNat.ofNat, Eq, IntermediateField.induction_on_adjoin
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h : Infinite F
β α : E
inr : ∃ (α_1 : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α_1⟯
⊢ ∃ (α_1 : E), Eq (α := IntermediateField F E) F⟮α_1⟯ (IntermediateField.restrictScalars F (L' := ↥F⟮α⟯) (↥F⟮α⟯)⟮β⟯)

Tactic:
simp_rw [adjoin_simple_adjoin_simple, eq_comm]

Premises used: IntermediateField.adjoin_simple_adjoin_simple, eq_comm
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h : Infinite F
β α : E
⊢ ∃ (α_1 : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α_1⟯

Tactic:
primitive_element_inf_aux_of_finite_intermediateField F α β

Premises used: _private.0.Field.primitive_element_inf_aux_of_finite_intermediateField
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite.{u_2 + 1} (IntermediateField F E)
K : IntermediateField F E
this : FiniteDimensional F E
h : Infinite F
β α : E
⊢ ∃ (α_1 : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α_1⟯

Tactic:
exact primitive_element_inf_aux_of_finite_intermediateField F α β

Premises used: _private.0.Field.primitive_element_inf_aux_of_finite_intermediateField
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
obtain : ∀ (α : E) (hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), FiniteDimensional F E
⊢ FiniteDimensional F E

Tactic:
obtain ⟨α, hprim⟩ := h
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
⊢ FiniteDimensional.{u_1, u_2} F ↥F⟮α⟯

Tactic:
have hfin := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) α)
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
hfin : FiniteDimensional.{u_1, u_2} F ↥F⟮α⟯
⊢ FiniteDimensional.{u_1, u_2} F ↥⊤

Tactic:
rw [hprim] at hfin
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
hfin : FiniteDimensional.{u_1, u_2} F ↥⊤
⊢ FiniteDimensional F E

Tactic:
topEquiv.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
hfin : FiniteDimensional.{u_1, u_2} F ↥⊤
⊢ FiniteDimensional F E

Tactic:
exact topEquiv.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
⊢ FiniteDimensional F E

Tactic:
haveI := FiniteDimensional.of_exists_primitive_element F E h
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
h : ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
this : FiniteDimensional F E
obtain : ∀ (α : E) (hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), Finite.{u_2 + 1} (IntermediateField F E)
⊢ Finite.{u_2 + 1} (IntermediateField F E)

Tactic:
obtain ⟨α, hprim⟩ := h
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
⊢ Finite G

Tactic:
have hfin : Finite G := @Finite.of_fintype _ <| fintypeSubtypeMonicDvd
    (f.map (algebraMap F E)) <| map_ne_zero (minpoly.ne_zero_of_finite F α)
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Dvd.dvd (α := E[X]) (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α))
    (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (Polynomial.map (algebraMap F ↥K) (minpoly F α)))

Tactic:
Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)

Premises used: Algebra.algebraMap, Polynomial.map_dvd, Membership.mem, Subtype, minpoly.dvd_map_of_isScalarTower
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
h :
  Eq (α := E[X]) (Polynomial.map (algebraMap F E) f)
    (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (Polynomial.map (algebraMap F ↥K) (minpoly F α)))
⊢ Dvd.dvd (α := E[X]) (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α))
    (Polynomial.map (algebraMap F E) f)

Tactic:
convert! Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)

Premises used: Algebra.algebraMap, Polynomial.map_dvd, Membership.mem, Subtype, minpoly.dvd_map_of_isScalarTower
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
h :
  Eq (α := E[X]) (Polynomial.map (algebraMap F E) f)
    (Polynomial.map (@RingHom.comp _ ↥K _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K) E) (algebraMap F ↥K))
      (minpoly F α))
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap F E) f)
    (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (Polynomial.map (algebraMap F ↥K) (minpoly F α)))

Tactic:
rw [Polynomial.map_map]

Premises used: Polynomial.map_map
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
K : IntermediateField F E
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap F E) f)
    (Polynomial.map (@RingHom.comp _ ↥K _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥K) E) (algebraMap F ↥K))
      (minpoly F α))

Tactic:
rfl
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G :=
  fun (K : IntermediateField F E) ↦
    Subtype.mk (p := fun (g : E[X]) ↦ g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f)
      (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)) ⋯
K K' : IntermediateField F E
heq : g K = g K'
⊢ Eq (α := E[X]) (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α))
    (Polynomial.map (R := ↥K') (algebraMap (↥K') E) (minpoly (↥K') α))

Tactic:
rw [Subtype.mk.injEq] at heq

Premises used: Subtype.mk.injEq
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G :=
  fun (K : IntermediateField F E) ↦
    Subtype.mk (p := fun (g : E[X]) ↦ g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f)
      (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)) ⋯
K K' : IntermediateField F E
heq :
  Eq (α := E[X]) (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α))
    (Polynomial.map (R := ↥K') (algebraMap (↥K') E) (minpoly (↥K') α))
⊢ Eq (α := IntermediateField F E)
    (adjoin F (↑(coeffs (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α))) : Set E))
    (adjoin F (↑(coeffs (Polynomial.map (R := ↥K') (algebraMap (↥K') E) (minpoly (↥K') α))) : Set E))

Tactic:
apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq

Premises used: SetLike.coe, Polynomial.coeffs, IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
this : FiniteDimensional F E
α : E
hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤
f : F[X] := minpoly F α
G : Type (max 0 u_2) := { g : E[X] // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }
hfin : Finite G
g : IntermediateField F E → G :=
  fun (K : IntermediateField F E) ↦
    Subtype.mk (p := fun (g : E[X]) ↦ g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f)
      (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α)) ⋯
K K' : IntermediateField F E
heq :
  Eq (α := IntermediateField F E)
    (adjoin F (↑(coeffs (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (minpoly (↥K) α))) : Set E))
    (adjoin F (↑(coeffs (Polynomial.map (R := ↥K') (algebraMap (↥K') E) (minpoly (↥K') α))) : Set E))
⊢ K = K'

Tactic:
simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq

Premises used: IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element