awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.PrimitiveElement
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) β
⊢ Eq (α := E[X]) (Polynomial.map (algebraMap (↥F⟮α + c • β⟯) 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) ⋯) :
                (↥F⟮γ⟯)[X])
              X))))
      (Polynomial.map (R := ↥F⟮γ⟯) (algebraMap (↥F⟮γ⟯) E) (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)))

Tactic:
convert! (gcd_map (algebraMap F⟮γ⟯ E)).symm

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Polynomial.gcd_map, IntermediateField.adjoin, Singleton.singleton, Eq.symm
-- Module: Mathlib.FieldTheory.PrimitiveElement
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) β
⊢ EuclideanDomain.gcd
      (comp (Polynomial.map (algebraMap F E) f)
        (HSub.hSub (α := E[X]) ((C : (a : E) → E[X]) γ : E[X])
          (HMul.hMul (α := E[X]) (β := E[X])
            ((C : (a : E) → E[X])
                ((algebraMap (↥F⟮γ⟯) E : (a : ↥F⟮γ⟯) → E)
                  (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x)
                      ((algebraMap F E : (a : F) → E) c) ⋯ :
                    ↥F⟮γ⟯)) :
              E[X])
            X)))
      (Polynomial.map (algebraMap F E) g) =
    h

Tactic:
congr
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 • β⟯
obtain : ∀ (x y : F) (hneq : x ≠ y) (heq : f x = f y), ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯

Tactic:
obtain ⟨x, y, hneq, heq⟩ := Finite.exists_ne_map_eq_of_infinite f

Premises used: Finite.exists_ne_map_eq_of_infinite
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯

Tactic:
use α + x • β
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 • β⟯
h₁ : LE.le (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α, β⟯
⊢ Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : {α, β} ⊆ (↑F⟮α + x • β⟯ : Set E)
⊢ LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮α + x • β⟯

Tactic:
rw [adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)

Tactic:
have αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯ := mem_adjoin_simple_self F _
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 • β)
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + y • β⟯ (α + y • β)

Tactic:
have αyβ_in_K : α + y • β ∈ F⟮α + y • β⟯ := mem_adjoin_simple_self F _
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + y • β⟯ (α + y • β)
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)

Tactic:
simp only [← heq] at αyβ_in_K
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - (α + y • β))

Tactic:
have β_in_K := sub_mem αxβ_in_K αyβ_in_K
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - (α + y • β))
rw : α + x • β - (α + y • β) = x • β - y • β
⊢ α + x • β - (α + y • β) = (x - y) • β

Tactic:
rw [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - (α + y • β))
⊢ α + x • β - (α + y • β) = x • β - y • β

Tactic:
abel1
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - (α + y • β))
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y) • β)

Tactic:
rw [show (α + x • β) - (α + y • β) = (x - y) • β by rw [sub_smul]; abel1] at β_in_K
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y) • β)
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y)⁻¹ • (x - y) • β)

Tactic:
replace β_in_K := smul_mem _ β_in_K (x := (x - y)⁻¹)
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ ((x - y)⁻¹ • (x - y) • β)
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ β

Tactic:
rw [smul_smul, inv_mul_eq_div, div_self (sub_ne_zero.2 hneq), one_smul] at β_in_K

Premises used: Iff.mpr, sub_ne_zero, inv_mul_eq_div, smul_smul, one_smul, div_self
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β - x • β)

Tactic:
sub_mem αxβ_in_K (smul_mem _ β_in_K)

Premises used: sub_mem, IntermediateField.smul_mem
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Eq (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + x • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ (α + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮α + x • β⟯ α

Tactic:
have α_in_K : α ∈ F⟮α + x • β⟯ := by
      convert! ← sub_mem αxβ_in_K (smul_mem _ β_in_K)
      apply add_sub_cancel_right
-- Module: Mathlib.FieldTheory.PrimitiveElement
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)
x_1 y : F
hneq : ¬x_1 = y
x : E
f : F → IntermediateField F E := fun (x_2 : F) ↦ F⟮x + x_2 • β⟯
heq : Eq (α := IntermediateField F E) F⟮x + x_1 • β⟯ F⟮x + y • β⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮x + x_1 • β⟯ (x + x_1 • β)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮x + x_1 • β⟯ (x + y • β)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮x + x_1 • β⟯ β
α_in_K : Membership.mem (γ := IntermediateField F E) F⟮x + x_1 • β⟯ x
⊢ x ∈ (↑F⟮x + x_1 • β⟯ : Set E)

Tactic:
assumption
-- Module: Mathlib.FieldTheory.PrimitiveElement
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)
x_1 y : F
hneq : ¬x_1 = y
x : E
f : F → IntermediateField F E := fun (x_2 : F) ↦ F⟮α + x_2 • x⟯
heq : Eq (α := IntermediateField F E) F⟮α + x_1 • x⟯ F⟮α + y • x⟯
αxβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x_1 • x⟯ (α + x_1 • x)
αyβ_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x_1 • x⟯ (α + y • x)
β_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x_1 • x⟯ x
α_in_K : Membership.mem (γ := IntermediateField F E) F⟮α + x_1 • x⟯ α
⊢ x ∈ (↑F⟮α + x_1 • x⟯ : Set E)

Tactic:
assumption
-- Module: Mathlib.FieldTheory.PrimitiveElement
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 : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ (α + x • β)
⊢ LE.le (α := IntermediateField F E) F⟮α + x • β⟯ F⟮α, β⟯

Tactic:
rw [adjoin_simple_le_iff]

Premises used: IntermediateField.adjoin_simple_le_iff
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α

Tactic:
have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
α_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ β

Tactic:
have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
α_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α
β_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ (α + x • β)

Tactic:
F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)

Premises used: IntermediateField.add_mem, Insert.insert, IntermediateField.smul_mem, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.FieldTheory.PrimitiveElement
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
α_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α
β_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ (α + x • β)

Tactic:
exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)

Premises used: IntermediateField.add_mem, Insert.insert, IntermediateField.smul_mem, 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
inl : ∀ (F_inf : IsEmpty.{u_1 + 1} (Fintype F)), ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
inr : ∀ (F_finite : Fintype F), ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤
⊢ ∃ (α : E), Eq (α := IntermediateField F E) F⟮α⟯ ⊤

Tactic:
rcases isEmpty_or_nonempty (Fintype F) with (F_inf | ⟨⟨F_finite⟩⟩)

Premises used: isEmpty_or_nonempty, Fintype
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
⊢ P ⊥

Tactic:
have base : P ⊥ := ⟨0, adjoin_zero⟩
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β : E
hK : P K
obtain : ∀ (α : E) (hK : F⟮α⟯ = K), P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮β⟯)
⊢ P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮β⟯)

Tactic:
obtain ⟨α, hK⟩ := hK
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
rw : P F⟮α, β⟯
⊢ P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮β⟯)

Tactic:
rw [← hK, adjoin_simple_adjoin_simple]

Premises used: IntermediateField.adjoin_simple_adjoin_simple
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
haveI : ∀ (this : Infinite F), P F⟮α, β⟯
⊢ P F⟮α, β⟯

Tactic:
haveI : Infinite F := isEmpty_fintype.mp F_inf
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
this : Infinite F
obtain : ∀ (γ : E) (hγ : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯), P F⟮α, β⟯
⊢ P F⟮α, β⟯

Tactic:
obtain ⟨γ, hγ⟩ := primitive_element_inf_aux F α β

Premises used: Field.primitive_element_inf_aux
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
this : Infinite F
γ : E
hγ : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
⊢ P F⟮α, β⟯

Tactic:
⟨γ, hγ.symm⟩

Premises used: Exists.intro, Eq.symm
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
this : Infinite F
γ : E
hγ : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
⊢ P F⟮α, β⟯

Tactic:
exact ⟨γ, hγ.symm⟩
-- 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 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
F_inf : IsEmpty.{u_1 + 1} (Fintype F)
P : IntermediateField F E → Prop := fun (K : IntermediateField F E) ↦ ∃ (α : E), F⟮α⟯ = K
base : P ⊥
⊢ ∀ (K : IntermediateField F E) (x : E), P K → P (IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)

Tactic:
have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F) := by
      intro K β hK
      obtain ⟨α, hK⟩ := hK
      rw [← hK, adjoin_simple_adjoin_simple]
      haveI : Infinite F := isEmpty_fintype.mp F_inf
      obtain ⟨γ, hγ⟩ := primitive_element_inf_aux F α β
      exact ⟨γ, hγ.symm⟩