awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h_root : eval β h = 0
⊢ 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_splits : (Polynomial.map ιEE' h).Splits
Tactic: have h_splits : Splits (h.map ιEE') := by
    rw [← Polynomial.gcd_map]
    exact (SplittingField.splits _).of_dvd (map_ne_zero map_g_ne_zero)
      (EuclideanDomain.gcd_dvd_right _ _)
-- 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
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : x ∈ (Polynomial.map ιEE' h).roots
⊢ x = (ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β
have hx₁ : eval₂ ιEE' x h = 0
Tactic: rw [mem_roots_map h_ne_zero] at hx
Cleared hypotheses: hx
-- 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
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
⊢ HSub.hSub (α := (Polynomial.map ιFE g).SplittingField)
      ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) γ : (Polynomial.map ιFE g).SplittingField)
      (HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
        ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((ιFE : (a : F) → E) c) :
          (Polynomial.map ιFE g).SplittingField)
        x) ∈
    (Polynomial.map (ιEE'.comp ιFE) f).roots
have f_root : eval₂ ιEE' x
    ((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
Tactic: have f_root := root_left_of_root_gcd hx
-- 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
γ : 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
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
hc :
  ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
    -HSub.hSub (β := (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)
              (HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
                ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((ιFE : (a : F) → E) c) :
                  (Polynomial.map ιFE g).SplittingField)
                x))
            ((ι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
⊢ x ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots
have rw : eval₂ ιEE' x (Polynomial.map ιFE (minpoly F β)) = 0
Tactic: rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
-- 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
γ : 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
h_splits : (Polynomial.map ιEE' h).Splits
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
hc :
  -HSub.hSub (β := (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)
            (HMul.hMul (α := (Polynomial.map ιFE g).SplittingField)
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) ((ιFE : (a : F) → E) c) :
                (Polynomial.map ιFE g).SplittingField)
              x))
          ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
      HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) x
        ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
    (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
⊢ x = (ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β
have by_contra : ∀ (a : ¬x = (ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β), False
Tactic: by_contra a
-- 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
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
⊢ 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_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = (ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β
Tactic: have h_roots : ∀ x ∈ (h.map ιEE').roots, x = ιEE' β := by
    intro x hx
    rw [mem_roots_map h_ne_zero] at hx
    specialize hc (ιEE' γ - ιEE' (ιFE c) * x) (by
      have f_root := root_left_of_root_gcd hx
      rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
      exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root)
    specialize hc x (by
      rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
      exact root_right_of_root_gcd hx)
    by_contra a
    apply hc
    apply (div_eq_iff (sub_ne_zero.mpr a)).mpr
    simp only [γ, Algebra.smul_def, map_add, map_mul, RingHom.comp_apply]
    ring
-- 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
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = (ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β
⊢ 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 rw : Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = h
Tactic: rw [← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots]
-- 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
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = (ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = h
have trans : Eq (α := E[X]) (Polynomial.map (algebraMap (↥F⟮γ⟯) E) p)
  (EuclideanDomain.gcd
    (Polynomial.map (algebraMap (↥F⟮γ⟯) E)
      (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) sorry) :
              (↥F⟮γ⟯)[X])
            X))))
    (Polynomial.map (R := ↥F⟮γ⟯) (algebraMap (↥F⟮γ⟯) E) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)))
Tactic: trans EuclideanDomain.gcd (?_ : E[X]) (?_ : E[X])
-- 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 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have obtain : ∀ (x y : F) (hneq : x ≠ y) (heq : f x = f y), ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
Tactic: obtain ⟨x, y, hneq, heq⟩ := Finite.exists_ne_map_eq_of_infinite f
-- 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 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have h : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯
Tactic: use α + x • β
-- 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 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯
have h : LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯
Tactic: apply le_antisymm
-- 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 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
h : LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯
⊢ Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯
have h₁ : LE.le (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α, β⟯
Tactic: apply le_antisymm
-- 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 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯
have h : {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
Tactic: rw [adjoin_le_iff]
-- 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 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
Tactic: have αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯ := mem_adjoin_simple_self F _
-- 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 : Finite.{u_2 + 1} (IntermediateField F E)
f : F → IntermediateField F E := fun (x : F) ↦ F⟮α + x • β⟯
x y : F
hneq : x ≠ y
heq : f x = f y
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
⊢ {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
have αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + y • β⟯ (α + y • β)
Tactic: have αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯ := mem_adjoin_simple_self F _