awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
simp_rw :
  ∀ (s : Set (IntermediateField F E)),
    s.Nonempty →
      DirectedOn (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) s →
        Membership.mem (γ := IntermediateField F E) (⨆ (a : (↑s : Type u_2)), (↑a : IntermediateField F E)) x →
          ∃ (x_1 : IntermediateField F E) (_ : x_1 ∈ s), x ∈ x_1
⊢ IsCompactElement (α := IntermediateField F E) F⟮x⟯

Tactic:
simp_rw [isCompactElement_iff_le_of_directed_sSup_le,
    adjoin_simple_le_iff, sSup_eq_iSup', ← exists_prop]

Premises used: exists_prop, IntermediateField.adjoin_simple_le_iff, CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le, sSup_eq_iSup'
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
s : Set (IntermediateField F E)
hne : s.Nonempty
hs : DirectedOn (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) s
hx : Membership.mem (γ := IntermediateField F E) (⨆ (a : (↑s : Type u_2)), (↑a : IntermediateField F E)) x
⊢ Nonempty.{u_2 + 1} (↑s : Type u_2)

Tactic:
have := hne.to_subtype
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
s : Set (IntermediateField F E)
hne : s.Nonempty
hs : DirectedOn (fun (x1 x2 : IntermediateField F E) ↦ x1 ≤ x2) s
hx : Membership.mem (γ := IntermediateField F E) (⨆ (a : (↑s : Type u_2)), (↑a : IntermediateField F E)) x
this : Nonempty.{u_2 + 1} (↑s : Type u_2)
rwa :
  ∀ (hx : x ∈ (↑(⨆ (a : (↑s : Type u_2)), (↑a : IntermediateField F E)) : Set E))
    (this : Nonempty.{u_2 + 1} (↑s : Type u_2)), ∃ (x_1 : IntermediateField F E) (_ : x_1 ∈ s), x ∈ x_1
rwa₁ :
  ∀
    (hx :
      Membership.mem (γ := Set E)
        (⋃ (i : { x : IntermediateField F E // x ∈ s }), (↑(↑i : IntermediateField F E) : Set E)) x)
    (this : Nonempty.{u_2 + 1} (↑s : Type u_2)), ∃ (x_1 : IntermediateField F E) (_ : x_1 ∈ s), x ∈ x_1
rwa₂ :
  ∀ (hx : ∃ (i : { x : IntermediateField F E // x ∈ s }), x ∈ (↑(↑i : IntermediateField F E) : Set E))
    (this : Nonempty.{u_2 + 1} (↑s : Type u_2)), ∃ (x_1 : IntermediateField F E) (_ : x_1 ∈ s), x ∈ x_1
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀
    (hx :
      ∃ (a : IntermediateField F E) (b : a ∈ s),
        x ∈ (↑(↑(Subtype.mk (p := fun (a : IntermediateField F E) ↦ a ∈ s) a b) : IntermediateField F E) : Set E))
    (this : Nonempty.{u_2 + 1} (↑s : Type u_2)), ∃ (x_1 : IntermediateField F E) (_ : x_1 ∈ s), x ∈ x_1
⊢ ∃ (x_1 : IntermediateField F E) (_ : x_1 ∈ s), x ∈ x_1

Tactic:
rwa [← SetLike.mem_coe, coe_iSup_of_directed hs.directed_val, mem_iUnion, Subtype.exists] at hx

Premises used: IntermediateField.coe_iSup_of_directed, Set.mem_iUnion, Subtype.exists, DirectedOn.directed_val, SetLike.mem_coe
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
rw : IsCompactElement.{u_2} (α := IntermediateField F E) (⨆ x ∈ (↑S : Set E), F⟮x⟯)
⊢ IsCompactElement (α := IntermediateField F E) (adjoin F (↑S : Set E))

Tactic:
rw [← biSup_adjoin_simple]

Premises used: IntermediateField.biSup_adjoin_simple
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
simp_rw : IsCompactElement (α := IntermediateField F E) (S.sup fun (a : E) ↦ F⟮a⟯)
⊢ IsCompactElement.{u_2} (α := IntermediateField F E) (⨆ x ∈ (↑S : Set E), F⟮x⟯)

Tactic:
simp_rw [Finset.mem_coe, ← Finset.sup_eq_iSup]

Premises used: Finset.sup_eq_iSup, Finset.mem_coe
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
⊢ IsCompactElement (α := IntermediateField F E) (S.sup fun (a : E) ↦ F⟮a⟯)

Tactic:
isCompactElement_finsetSup S fun x _ => adjoin_simple_isCompactElement x

Premises used: CompleteLattice.isCompactElement_finsetSup, IntermediateField.adjoin_simple_isCompactElement
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Finset E
⊢ IsCompactElement (α := IntermediateField F E) (S.sup fun (a : E) ↦ F⟮a⟯)

Tactic:
exact isCompactElement_finsetSup S fun x _ => adjoin_simple_isCompactElement x

Premises used: CompleteLattice.isCompactElement_finsetSup, IntermediateField.adjoin_simple_isCompactElement
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
h : S.Finite
⊢ IsCompactElement (α := IntermediateField F E) (adjoin F S)

Tactic:
Finite.coe_toFinset h ▸ adjoin_finset_isCompactElement h.toFinset

Premises used: Eq.rec, Set.Finite.coe_toFinset, Set.Finite.toFinset, IntermediateField.adjoin_finset_isCompactElement
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
s : IntermediateField F E
x : E
left : x ∈ (↑s : Set E)
⊢ IsCompactElement.{u_2} (α := IntermediateField F E) ((fun (x : E) ↦ (F⟮x⟯ : IntermediateField F E)) x)

Tactic:
adjoin_simple_isCompactElement x

Premises used: IntermediateField.adjoin_simple_isCompactElement
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
s : IntermediateField F E
x : E
left : x ∈ (↑s : Set E)
⊢ IsCompactElement.{u_2} (α := IntermediateField F E) ((fun (x : E) ↦ (F⟮x⟯ : IntermediateField F E)) x)

Tactic:
exact adjoin_simple_isCompactElement x

Premises used: IntermediateField.adjoin_simple_isCompactElement
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
⊢ ∀ (h : LE.le (α := IntermediateField F E) F⟮x⟯ (⨆ (i : ι), f i)),
    ∃ (s : Finset ι), LE.le (α := IntermediateField F E) F⟮x⟯ (⨆ i ∈ s, f i)

Tactic:
have := (adjoin_simple_isCompactElement x).exists_finset_of_le_iSup (IntermediateField F E) f
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
this :
  ∀ (h : LE.le (α := IntermediateField F E) F⟮x⟯ (⨆ (i : ι), f i)),
    ∃ (s : Finset ι), LE.le (α := IntermediateField F E) F⟮x⟯ (⨆ i ∈ s, f i)
⊢ ∀ (h : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x),
    ∃ (s : Finset ι), Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, f i) x

Tactic:
simp only [adjoin_simple_le_iff] at this

Premises used: IntermediateField.adjoin_simple_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
this :
  ∀ (h : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x),
    ∃ (s : Finset ι), Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, f i) x
⊢ ∃ (s : Finset ι), Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, f i) x

Tactic:
this hx
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
this :
  ∀ (h : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x),
    ∃ (s : Finset ι), Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, f i) x
⊢ ∃ (s : Finset ι), Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, f i) x

Tactic:
exact this hx
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
⊢ ∃ (s : Finset ((i : ι) × ↥(f i))),
    Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(f i))) : E)⟯) x

Tactic:
exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le fun i x h ↦ ?_) hx)

Premises used: SetLike.le_def, IntermediateField.exists_finset_of_mem_iSup, Iff.mp, iSup_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
refine :
  ∀ (i : ι) (x : E) (h : x ∈ f i),
    Membership.mem (γ := IntermediateField F E)
      (⨆ (i : (i : ι) × ↥(f i)), F⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(f i))) : E)⟯) x
⊢ ∃ (s : Finset ((i : ι) × ↥(f i))),
    Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(f i))) : E)⟯) x

Tactic:
refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le fun i x h ↦ ?_) hx)

Premises used: SetLike.le_def, IntermediateField.exists_finset_of_mem_iSup, Iff.mp, iSup_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x_1 : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x_1
i : ι
x : E
h : x ∈ f i
⊢ LE.le (α := IntermediateField F E) F⟮x⟯
    F⟮(↑(Sigma.snd (β := fun (i : ι) ↦ ↥(f i))
            (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x h))) :
        E)⟯

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x_1 : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x_1
i : ι
x : E
h : x ∈ f i
⊢ Membership.mem (γ := IntermediateField F E) (⨆ (i : (i : ι) × ↥(f i)), F⟮(↑(i.snd (β := fun (i : ι) ↦ ↥(f i))) : E)⟯)
    x

Tactic:
exact SetLike.le_def.mp (le_iSup_of_le ⟨i, x, h⟩ (by simp)) (mem_adjoin_simple_self F x)

Premises used: IntermediateField.mem_adjoin_simple_self, SetLike.le_def, le_iSup_of_le, Iff.mp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
⊢ ∃ (s : Finset ((i : ι) × ↥(f i))),
    Membership.mem (γ := IntermediateField F E)
      (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(f i)))) E)) x

Tactic:
exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le (fun i x1 hx1 => ?_)) hx)

Premises used: SetLike.le_def, IntermediateField.exists_finset_of_mem_iSup, Iff.mp, iSup_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
refine :
  ∀ (i : ι) (x1 : E) (hx1 : x1 ∈ f i),
    Membership.mem (γ := IntermediateField F E)
      (⨆ (i : (i : ι) × ↥(f i)), adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(f i)))) E)) x1
⊢ ∃ (s : Finset ((i : ι) × ↥(f i))),
    Membership.mem (γ := IntermediateField F E)
      (⨆ i ∈ s, adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(f i)))) E)) x

Tactic:
refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le (fun i x1 hx1 => ?_)) hx)

Premises used: SetLike.le_def, IntermediateField.exists_finset_of_mem_iSup, Iff.mp, iSup_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ Membership.mem (γ := IntermediateField F E)
    (⨆ (i : (i : ι) × ↥(f i)), adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(f i)))) E)) x1

Tactic:
SetLike.le_def.mp (le_iSup_of_le ⟨i, x1, hx1⟩ ?_)
    (subset_adjoin F (rootSet (minpoly F x1) E) ?_)

Premises used: Set.Mem, setOf, Polynomial.rootSet, SetLike.le_def, IntermediateField.subset_adjoin, minpoly, le_iSup_of_le, Iff.mp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
i : ι
x1 : E
hx1 : x1 ∈ f i
refine_1 :
  LE.le (α := IntermediateField F E) (adjoin F (rootSet (minpoly F x1) E))
    (adjoin F
      (rootSet
        (minpoly.{u_1, u_2} F (B :=
          ↥(f
              (Sigma.fst (β := fun (i : ι) ↦ ↥(f i))
                (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x1 hx1)))))
          (Sigma.snd (β := fun (i : ι) ↦ ↥(f i))
              (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x1 hx1)) :
            ↥(f
                (Sigma.fst (β := fun (i : ι) ↦ ↥(f i))
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x1 hx1))))))
        E))
refine_2 : x1 ∈ rootSet (minpoly F x1) E
⊢ Membership.mem (γ := IntermediateField F E)
    (⨆ (i : (i : ι) × ↥(f i)), adjoin F (rootSet (minpoly F (i.snd (β := fun (i : ι) ↦ ↥(f i)))) E)) x1

Tactic:
refine SetLike.le_def.mp (le_iSup_of_le ⟨i, x1, hx1⟩ ?_)
    (subset_adjoin F (rootSet (minpoly F x1) E) ?_)

Premises used: Polynomial.rootSet, SetLike.le_def, IntermediateField.subset_adjoin, minpoly, le_iSup_of_le, Iff.mp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
i : ι
x1 : E
hx1 : x1 ∈ f i
refine_1 :
  LE.le (α := IntermediateField F E) (adjoin F (rootSet (minpoly F x1) E))
    (adjoin F
      (rootSet
        (minpoly.{u_1, u_2} F (B := E)
          (↑(Sigma.snd (β := fun (i : ι) ↦ ↥(f i))
                (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x1 hx1))) :
            E))
        E))
refine_1₁ refine_1₂ :
  LE.le (α := IntermediateField F E) (adjoin F (rootSet (minpoly F x1) E)) (adjoin F (rootSet (minpoly F x1) E))
⊢ LE.le (α := IntermediateField F E) (adjoin F (rootSet (minpoly F x1) E))
    (adjoin F
      (rootSet
        (minpoly.{u_1, u_2} F (B :=
          ↥(f
              (Sigma.fst (β := fun (i : ι) ↦ ↥(f i))
                (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x1 hx1)))))
          (Sigma.snd (β := fun (i : ι) ↦ ↥(f i))
              (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x1 hx1)) :
            ↥(f
                (Sigma.fst (β := fun (i : ι) ↦ ↥(f i))
                  (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i (Subtype.mk (p := fun (x : E) ↦ x ∈ f i) x1 hx1))))))
        E))

Tactic:
rw [IntermediateField.minpoly_eq, Subtype.coe_mk]

Premises used: Subtype.coe_mk, IntermediateField.minpoly_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
i : ι
x1 : E
hx1 : x1 ∈ f i
refine_2 : Ne (α := F[X]) (minpoly F x1) 0
⊢ x1 ∈ rootSet (minpoly F x1) E

Tactic:
rw [mem_rootSet_of_ne, minpoly.aeval]

Premises used: minpoly.aeval, Polynomial.mem_rootSet_of_ne
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ Ne (α := F[X]) (minpoly F x1) 0

Tactic:
minpoly.ne_zero (isIntegral_iff.mp (Algebra.IsIntegral.isIntegral (⟨x1, hx1⟩ : f i)))

Premises used: Algebra.IsIntegral.isIntegral, Subtype.mk, Iff.mp, minpoly.ne_zero, IntermediateField.isIntegral_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsAlgebraic.{u_1, u_2} F ↥(f i)
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : ι), f i) x
i : ι
x1 : E
hx1 : x1 ∈ f i
⊢ Ne (α := F[X]) (minpoly F x1) 0

Tactic:
exact minpoly.ne_zero (isIntegral_iff.mp (Algebra.IsIntegral.isIntegral (⟨x1, hx1⟩ : f i)))

Premises used: Algebra.IsIntegral.isIntegral, Subtype.mk, Iff.mp, minpoly.ne_zero, IntermediateField.isIntegral_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
⊢ Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x

Tactic:
simp_rw [← biSup_adjoin_simple S, ← iSup_subtype''] at hx

Premises used: iSup_subtype'', IntermediateField.biSup_adjoin_simple
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
obtain :
  ∀ (s : Finset (↑S : Type u_2)) (hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x),
    ∃ (T : Finset E), (↑T : Set E) ⊆ S ∧ Membership.mem (γ := IntermediateField F E) (adjoin F (↑T : Set E)) x
⊢ ∃ (T : Finset E), (↑T : Set E) ⊆ S ∧ Membership.mem (γ := IntermediateField F E) (adjoin F (↑T : Set E)) x

Tactic:
obtain ⟨s, hx'⟩ := exists_finset_of_mem_iSup hx

Premises used: IntermediateField.exists_finset_of_mem_iSup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
s : Finset (↑S : Type u_2)
hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x
⊢ (↑(Finset.image (Subtype.val (p := fun (x : E) ↦ x ∈ S)) s) : Set E) ⊆ S

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
s : Finset (↑S : Type u_2)
hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x
refine :
  LE.le (α := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯)
    (adjoin F (↑(Finset.image (Subtype.val (p := fun (x : E) ↦ x ∈ S)) s) : Set E))
⊢ ∃ (T : Finset E), (↑T : Set E) ⊆ S ∧ Membership.mem (γ := IntermediateField F E) (adjoin F (↑T : Set E)) x

Tactic:
refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
s : Finset (↑S : Type u_2)
hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x
simp_rw :
  ∀ (i : (↑S : Type u_2)) (i_1 : i ∈ s),
    {(↑i : E)} ⊆ (↑(adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ S) '' (↑s : Set { x : E // x ∈ S }))) : Set E)
⊢ LE.le (α := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯)
    (adjoin F (↑(Finset.image (Subtype.val (p := fun (x : E) ↦ x ∈ S)) s) : Set E))

Tactic:
simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff, Finset.coe_image, iSup_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
s : Finset (↑S : Type u_2)
hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x
i : (↑S : Type u_2)
h : i ∈ s
⊢ (↑i : E) ∈ (↑(adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ S) '' (↑s : Set { x : E // x ∈ S }))) : Set E)

Tactic:
subset_adjoin F _ ⟨_, h, rfl⟩

Premises used: IntermediateField.subset_adjoin, And.intro, Exists.intro, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
s : Finset (↑S : Type u_2)
hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x
i : (↑S : Type u_2)
h : i ∈ s
⊢ (↑i : E) ∈ (↑(adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ S) '' (↑s : Set { x : E // x ∈ S }))) : Set E)

Tactic:
exact subset_adjoin F _ ⟨_, h, rfl⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (⨆ (i : (↑S : Type u_2)), F⟮(↑i : E)⟯) x
s : Finset (↑S : Type u_2)
hx' : Membership.mem (γ := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯) x
refine :
  LE.le (α := IntermediateField F E) (⨆ i ∈ s, F⟮(↑i : E)⟯)
    (adjoin F (↑(Finset.image (Subtype.val (p := fun (x : E) ↦ x ∈ S)) s) : Set E))
refine₁ :
  ∀ (i : (↑S : Type u_2)) (i_1 : i ∈ s),
    {(↑i : E)} ⊆ (↑(adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ S) '' (↑s : Set { x : E // x ∈ S }))) : Set E)
refine₂ :
  ∀ (i : (↑S : Type u_2)) (h : i ∈ s),
    (↑i : E) ∈ (↑(adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ S) '' (↑s : Set { x : E // x ∈ S }))) : Set E)
⊢ ∃ (T : Finset E), (↑T : Set E) ⊆ S ∧ Membership.mem (γ := IntermediateField F E) (adjoin F (↑T : Set E)) x

Tactic:
classical
  refine ⟨s.image Subtype.val, by simp, SetLike.le_def.mp ?_ hx'⟩
  simp_rw [Finset.coe_image, iSup_le_iff, adjoin_le_iff]
  rintro _ h _ rfl
  exact subset_adjoin F _ ⟨_, h, rfl⟩

Premises used: IntermediateField.adjoin_le_iff, Finset.coe_image, iSup_le_iff, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : Module.rank F ↥K = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₁ : Module.rank F ↥K.toSubalgebra = 1 ↔ K.toSubalgebra = toSubalgebra ⊥
rw₂ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = toSubalgebra ⊥
rw₃ rw₄ : K.toSubalgebra = ⊥ ↔ K.toSubalgebra = ⊥
⊢ Module.rank F ↥K = 1 ↔ K = ⊥

Tactic:
rw [← toSubalgebra_inj, ← rank_eq_rank_subalgebra, Subalgebra.rank_eq_one_iff,
    bot_toSubalgebra]

Premises used: IntermediateField.bot_toSubalgebra, Subalgebra.rank_eq_one_iff, IntermediateField.toSubalgebra_inj, IntermediateField.rank_eq_rank_subalgebra