awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
hf :
  eval
      (eval β
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
      (Polynomial.map ιFE f) =
    0
⊢ eval β
      ((Polynomial.map ιFE f).comp
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))) =
    0
have hf₁ : eval
    (eval β ((C : (a : E) → E[X]) γ) -
      eval β (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))
    (Polynomial.map ιFE f) =
  0
Tactic: rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
hf :
  eval
      (eval β
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
      (Polynomial.map ιFE f) =
    0
hf₁ :
  eval
      (eval β ((C : (a : E) → E[X]) γ) -
        eval β (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))
      (Polynomial.map ιFE f) =
    0
⊢ eval β
      ((Polynomial.map ιFE f).comp
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))) =
    0
have hf₂ : eval (eval β ((C : (a : E) → E[X]) γ) - eval β ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c)) * eval β X)
    (Polynomial.map ιFE f) =
  0
Tactic: rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
hf :
  eval
      (eval β
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
      (Polynomial.map ιFE f) =
    0
hf₁ :
  eval
      (eval β ((C : (a : E) → E[X]) γ) -
        eval β (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))
      (Polynomial.map ιFE f) =
    0
hf₂ :
  eval (eval β ((C : (a : E) → E[X]) γ) - eval β ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c)) * eval β X)
      (Polynomial.map ιFE f) =
    0
⊢ eval β
      ((Polynomial.map ιFE f).comp
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))) =
    0
have hf₃ : eval (γ - eval β ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c)) * eval β X) (Polynomial.map ιFE f) = 0
Tactic: rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
hf :
  eval
      (eval β
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
      (Polynomial.map ιFE f) =
    0
hf₁ :
  eval
      (eval β ((C : (a : E) → E[X]) γ) -
        eval β (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))
      (Polynomial.map ιFE f) =
    0
hf₂ :
  eval (eval β ((C : (a : E) → E[X]) γ) - eval β ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c)) * eval β X)
      (Polynomial.map ιFE f) =
    0
hf₃ : eval (γ - eval β ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c)) * eval β X) (Polynomial.map ιFE f) = 0
⊢ eval β
      ((Polynomial.map ιFE f).comp
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))) =
    0
have hf₄ : eval (γ - HMul.hMul (α := E) ((ιFE : (a : F) → E) c : E) (eval β X)) (Polynomial.map ιFE f) = 0
Tactic: rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
hf :
  eval
      (eval β
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
      (Polynomial.map ιFE f) =
    0
hf₁ :
  eval
      (eval β ((C : (a : E) → E[X]) γ) -
        eval β (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))
      (Polynomial.map ιFE f) =
    0
hf₂ :
  eval (eval β ((C : (a : E) → E[X]) γ) - eval β ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c)) * eval β X)
      (Polynomial.map ιFE f) =
    0
hf₃ : eval (γ - eval β ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c)) * eval β X) (Polynomial.map ιFE f) = 0
hf₄ : eval (γ - HMul.hMul (α := E) ((ιFE : (a : F) → E) c : E) (eval β X)) (Polynomial.map ιFE f) = 0
⊢ eval β
      ((Polynomial.map ιFE f).comp
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))) =
    0
have hf₅ : eval (γ - HMul.hMul (α := E) ((ιFE : (a : F) → E) c : E) β) (Polynomial.map ιFE f) = 0
Tactic: rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β (Polynomial.map ιFE g) = 0
have hg : Eq.{u_2 + 1} (α := E) ((aeval β : (a : F[X]) → E) g : E) (0 : E)
Tactic: rw [eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
hg : Eq.{u_2 + 1} (α := E) ((aeval β : (a : F[X]) → E) g : E) (0 : E)
⊢ eval β (Polynomial.map ιFE g) = 0
have hg₁ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p =
    HMul.hMul (α := E[X]) ((C : (a : E) → E[X]) h.leadingCoeff : E[X])
      (HSub.hSub (α := E[X]) (β := E[X]) X ((C : (a : E) → E[X]) β : E[X]))
have h_root : eval β h = 0
Tactic: have h_root : h.eval β = 0 := by
    apply eval_gcd_eq_zero
    · rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map_algebraMap, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
    · rw [eval_map_algebraMap, minpoly.aeval]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F ↥F⟮γ⟯) f)
      (HSub.hSub (α := (↥F⟮γ⟯)[X]) ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X]) (AdjoinSimple.gen F γ) : (↥F⟮γ⟯)[X])
        (HMul.hMul (α := (↥F⟮γ⟯)[X]) (β := (↥F⟮γ⟯)[X])
          ((C : (a : ↥F⟮γ⟯) → (↥F⟮γ⟯)[X])
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                ((algebraMap F E : (a : F) → E) c) ⋯) :
            (↥F⟮γ⟯)[X])
          X)))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map ιFE f).comp
      (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
        (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X)))
    (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
⊢ (Polynomial.map ιEE' h).Splits
have rw : (EuclideanDomain.gcd
    (Polynomial.map ιEE'
      ((Polynomial.map ιFE f).comp
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X]) ((C : (a : E) → E[X]) ((ιFE : (a : F) → E) c) : E[X]) X))))
    (Polynomial.map ιEE' (Polynomial.map ιFE g))).Splits
Tactic: rw [← Polynomial.gcd_map]