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
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
obtain :
  ∀ (c : F) (hc : c ∉ s'),
    ∃ (c : F),
      ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c

Tactic:
obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'

Premises used: Infinite.exists_notMem_finset
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
c : F
hc : c ∉ s'
⊢ ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = (ϕ : (a : F) → E) c

Tactic:
simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc

Premises used: Multiset.mem_map, Finset.mem_preimage, Multiset.mem_bind, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
c : F
hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = (ϕ : (a : F) → E) c
⊢ ∀ (a : E) (_ : a ∈ sf) (a_1 : E) (_ : a_1 ∈ sg), -(a - α) / (a_1 - β) ≠ (ϕ : (a : F) → E) c

Tactic:
push Not at hc

Premises used: Not
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
c : F
hc : ∀ (a : E) (_ : a ∈ sf) (a_1 : E) (_ : a_1 ∈ sg), -(a - α) / (a_1 - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c

Tactic:
⟨c, hc⟩

Premises used: Exists.intro
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
c : F
hc : ∀ (a : E) (_ : a ∈ sf) (a_1 : E) (_ : a_1 ∈ sg), -(a - α) / (a_1 - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c

Tactic:
exact ⟨c, hc⟩
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
let let₁ let₂ let₃ :
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
let₄ :
  let s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg);
  let s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯;
  ∀ (c : F) (hc : c ∉ s'),
    ∃ (c : F),
      ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
let₅ :
  ∀ (c : F) (hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = (ϕ : (a : F) → E) c),
    ∃ (c : F),
      ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
let₆ :
  ∀ (c : F) (hc : ∀ (a : E) (_ : a ∈ sf) (a_1 : E) (_ : a_1 ∈ sg), -(a - α) / (a_1 - β) ≠ (ϕ : (a : F) → E) c),
    ∃ (c : F),
      ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c

Tactic:
classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push Not at hc
  exact ⟨c, hc⟩

Premises used: Multiset.mem_map, Finset.mem_preimage, Multiset.mem_bind, Not, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.PrimitiveElement
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
let let₁ let₂ let₃ :
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c

Tactic:
classical
  let sf := (f.map ϕ).roots
  let sg := (g.map ϕ).roots
  classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push Not at hc
  exact ⟨c, hc⟩

Premises used: Multiset.mem_map, Finset.mem_preimage, Multiset.mem_bind, Not, Multiset.mem_toFinset
-- 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
⊢ IsIntegral F α

Tactic:
have hα := Algebra.IsSeparable.isIntegral 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 : Algebra.IsSeparable F E
hα : IsIntegral F α
⊢ IsIntegral F β

Tactic:
have hβ := Algebra.IsSeparable.isIntegral 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 : 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
obtain :
  ∀ (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), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯

Tactic:
obtain ⟨c, hc⟩ := primitive_element_inf_aux_exists_c (ιEE'.comp ιFE) (ιEE' α) (ιEE' β) f g

Premises used: RingHom.comp, Field.primitive_element_inf_aux_exists_c, DFunLike.coe
-- 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
h : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯

Tactic:
use γ
-- 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
h : LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
h₁ : LE.le (α := IntermediateField F E) F⟮γ⟯ F⟮α, β⟯
⊢ Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯

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 : 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
h : {α, β} ⊆ (↑F⟮γ⟯ : Set E)
⊢ LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯

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 : 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
rw : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ (α + c • β - c • β)
⊢ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ α

Tactic:
rw [← add_sub_cancel_right α (c • β)]

Premises used: HSMul.hSMul, 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 : 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ (α + c • β - c • β)

Tactic:
F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)

Premises used: IntermediateField.mem_adjoin_simple_self, Subalgebra.smul_mem, IntermediateField.sub_mem, IntermediateField.adjoin, Singleton.singleton, IntermediateField.toSubalgebra
-- 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ (α + c • β - c • β)

Tactic:
exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)

Premises used: IntermediateField.mem_adjoin_simple_self, Subalgebra.smul_mem, IntermediateField.sub_mem, IntermediateField.adjoin, Singleton.singleton, IntermediateField.toSubalgebra
-- 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ α

Tactic:
have α_in_Fγ : α ∈ F⟮γ⟯ := by
        rw [← add_sub_cancel_right α (c • β)]
        exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)
-- 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 β
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
x : E
hα : IsIntegral F x
f : F[X] := minpoly F x
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) x : (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 := x + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
α_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x
⊢ x ∈ (↑F⟮γ⟯ : 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 : Algebra.IsSeparable F E
hα : IsIntegral F α
f : F[X] := minpoly F α
ιFE : F →+* E := algebraMap F E
c : F
x : E
hβ : IsIntegral F x
g : F[X] := minpoly F x
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
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) x : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • x
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ x
α_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ α
⊢ x ∈ (↑F⟮γ⟯ : 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 : 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
h : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ γ
⊢ LE.le (α := IntermediateField F E) F⟮γ⟯ 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 : 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 • β
β_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 α {β})
-- 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 • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
α_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)