awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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])
⊢ 0 < n
have linarith : n ≤ 0 →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) (↑n : ℤ) 0 + (HAdd.hAdd (α := ℤ) 0 1 - (↑m : ℤ)) +
      (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - (↑n : ℤ)) =
    0
Tactic: linarith only [hm, hmn]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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])
linarith :
  n ≤ 0 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) (↑n : ℤ) 0 + (HAdd.hAdd (α := ℤ) 0 1 - (↑m : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - (↑n : ℤ)) =
      0
⊢ 0 < n
have linarith₁ : n ≤ 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith only [hm, hmn]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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
have hn : 0 < n
Tactic: have hn : 0 < n := by linarith only [hm, hmn]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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
⊢ ¬n ∣ n * s.natDegree + m
have rw : ¬n ∣ m
Tactic: rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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
⊢ f.coeff (n * s.natDegree + m) ≠ 0
have hndvd : ¬n ∣ n * s.natDegree + m
Tactic: 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
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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
⊢ f.coeff (n * s.natDegree + m) ≠ 0
have simp : s.leadingCoeff ≠ 0
Tactic: 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]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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 ≠ 0
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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⟯ }
⊢ FiniteDimensional F E
have this : Algebra.IsAlgebraic F E
Tactic: have := isAlgebraic_of_finite_intermediateField F E
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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
⊢ FiniteDimensional F E
have this₁ : ∀ (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 _)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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 F E
have hfin : 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)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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))
⊢ FiniteDimensional F E
have htop : 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
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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 F E
have hfin₁ : FiniteDimensional.{u_1, u_2} F ↥⊤
Tactic: rw [htop] at hfin
Cleared hypotheses: hfin, htop
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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
⊢ ∃ (α : E), F⟮α⟯ = K
have this : FiniteDimensional F E
Tactic: haveI := FiniteDimensional.of_finite_intermediateField F E
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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
⊢ ∃ (α : E), F⟮α⟯ = K
have inl : Finite F → ∃ (α : E), F⟮α⟯ = K
Tactic: rcases finite_or_infinite F with (_ | _)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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
⊢ ∃ (α : E), F⟮α⟯ = K
have inr : Infinite F → ∃ (α : E), F⟮α⟯ = K
Tactic: rcases finite_or_infinite F with (_ | _)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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
⊢ ∃ (α : E), F⟮α⟯ = K
have inl : ∀ (α : ↥K) (h : Eq (α := IntermediateField F ↥K) F⟮α⟯ ⊤), ∃ (α : E), F⟮α⟯ = K
Tactic: obtain ⟨α, h⟩ := exists_primitive_element_of_finite_bot F K
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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), F⟮α⟯ = K
have inr : ∀ (K : IntermediateField F E) (x : E),
  (∃ (α : E), F⟮α⟯ = K) →
    ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
Tactic: apply induction_on_adjoin (fun K ↦ ∃ α : E, F⟮α⟯ = K) ⟨0, adjoin_zero⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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⟮α_1⟯ (IntermediateField.restrictScalars F (L' := ↥F⟮α⟯) (↥F⟮α⟯)⟮β⟯)
have inr : ∃ (α_1 : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α_1⟯
Tactic: simp_rw [adjoin_simple_adjoin_simple, eq_comm]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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
have obtain : ∀ (α : E) (hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), FiniteDimensional F E
Tactic: obtain ⟨α, hprim⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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 F E
have hfin : FiniteDimensional.{u_1, u_2} F ↥F⟮α⟯
Tactic: have hfin := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) α)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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 F E
have hfin₁ : FiniteDimensional.{u_1, u_2} F ↥⊤
Tactic: rw [hprim] at hfin
Cleared hypotheses: hfin
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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⟮α⟯ ⊤
⊢ Finite.{u_2 + 1} (IntermediateField F E)
have this : FiniteDimensional F E
Tactic: haveI := FiniteDimensional.of_exists_primitive_element F E h
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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
⊢ Finite.{u_2 + 1} (IntermediateField F E)
have obtain : ∀ (α : E) (hprim : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), Finite.{u_2 + 1} (IntermediateField F E)
Tactic: obtain ⟨α, hprim⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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.{u_2 + 1} (IntermediateField F E)
have hfin : 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 α)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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 (algebraMap F E) f)
have h : Eq (α := E[X]) (Polynomial.map (algebraMap F E) f)
  (Polynomial.map (R := ↥K) (algebraMap (↥K) E) (Polynomial.map (algebraMap F ↥K) (minpoly F α)))
Tactic: convert! Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
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 (R := ↥K) (algebraMap (↥K) E) (Polynomial.map (algebraMap F ↥K) (minpoly F α)))
have 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 α))
Tactic: rw [Polynomial.map_map]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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'
⊢ K = K'
have heq₁ : 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
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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') α))
⊢ K = K'
have 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))
Tactic: apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
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) α)) ⋯
⊢ Finite.{u_2 + 1} (IntermediateField F E)
have hinj : Function.Injective g
Tactic: have hinj : Function.Injective g := fun K K' heq ↦ by
    rw [Subtype.mk.injEq] at heq
    apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
    simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
L : Type u_3
inst_5 : Field L
inst_6 : Algebra F L
hL : ∀ (x : E), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ Fintype.card (E →ₐ[F] L) = finrank F E
have rw : Nat.card (E →ₐ[F] L) = finrank F E
Tactic: rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_splits F E L hL]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
L : Type u_3
inst_5 : Field L
inst_6 : Algebra F L
hL : ∀ (x : E), Splits (Polynomial.map (algebraMap F L) (minpoly F x))
rw : Nat.card (E →ₐ[F] L) = finrank F E
⊢ Fintype.card (E →ₐ[F] L) = finrank F E
have rw₁ : finrank F E = finrank F E
Tactic: rw [Fintype.card_eq_nat_card, AlgHom.natCard_of_splits F E L hL]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ natDegree (minpoly F α) = finrank F E
have rw : Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤
Tactic: rw [← adjoin.finrank (IsIntegral.of_finite F α), ← finrank_top F E]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤
have refine : ∀ (h : Eq (α := IntermediateField F E) F⟮α⟯ ⊤), finrank.{u_3, u_4} F ↥F⟮α⟯ = finrank.{u_3, u_4} F ↥⊤
Tactic: refine ⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
α : E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ degree (minpoly F α) = (↑(finrank F E) : WithBot ℕ)
have rw : Ne (α := F[X]) (minpoly F α) 0
Tactic: rw [degree_eq_iff_natDegree_eq, primitive_element_iff_minpoly_natDegree_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₁ : Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
  Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]