awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
ih : finrank.{u_1, u_2} F ↥(↥K)⟮x⟯ = finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
⊢ Nat.card.{u_2} (↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) →ₐ[F] E) =
    finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)

Tactic:
rw [of_separable_splitting_field_aux hp K (Multiset.mem_toFinset.mp hx), hK, finrank_mul_finrank]

Premises used: Membership.mem, Subtype, Module.finrank_mul_finrank, Iff.mp, IsGalois.of_separable_splitting_field_aux, Multiset.mem_toFinset
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
ih : finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) = finrank.{u_1, u_2} F ↥(↥K)⟮x⟯
⊢ finrank.{u_1, u_2} F ↥(↥K)⟮x⟯ = finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯)

Tactic:
symm
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
⊢ finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) = finrank.{u_1, u_2} F ↥(↥K)⟮x⟯

Tactic:
LinearEquiv.finrank_eq ?_

Premises used: LinearEquiv.finrank_eq
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
ih : ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) ≃ₗ[F] ↥(↥K)⟮x⟯
⊢ finrank.{u_1, u_2} F ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) = finrank.{u_1, u_2} F ↥(↥K)⟮x⟯

Tactic:
refine LinearEquiv.finrank_eq ?_

Premises used: LinearEquiv.finrank_eq
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : Eq (α := IntermediateField F E) (adjoin F s) ⊤
P : IntermediateField F E → Prop :=
  fun (K : IntermediateField F E) ↦ Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Nat.card.{u_2} (↥K →ₐ[F] E) = finrank.{u_1, u_2} F ↥K
⊢ ↥(IntermediateField.restrictScalars F (L' := ↥K) (↥K)⟮x⟯) ≃ₗ[F] ↥(↥K)⟮x⟯

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
⊢ IsGalois F E

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
⊢ ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
⊢ ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥

Tactic:
tfae_have 1 → 2 := fun h ↦ OrderIso.map_bot (@intermediateFieldEquivSubgroup F _ E _ _ _ h).symm

Premises used: OrderIso.symm, IsGalois.intermediateFieldEquivSubgroup, OrderIso.map_bot
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ IsGalois F E

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E

Tactic:
1 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
⊢ ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E

Tactic:
tfae_have 1 → 3 := fun _ ↦ card_aut_eq_finrank F E
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ IsGalois F E

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p

Tactic:
1 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
⊢ ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p

Tactic:
tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ IsGalois F E

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E

Tactic:
tfae_have 2 → 1 := of_fixedField_eq_bot F E

Premises used: IsGalois.of_fixedField_eq_bot
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
⊢ Nat.card.{u_2} Gal(E/F) = finrank F E

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
⊢ IsGalois F E

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
⊢ ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
⊢ ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E

Tactic:
tfae_have 3 → 1 := of_card_aut_eq_finrank F E

Premises used: IsGalois.of_card_aut_eq_finrank
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
tfae_3_to_1 : ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E
⊢ ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
tfae_3_to_1 : ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E
⊢ IsGalois F E

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
tfae_3_to_1 : ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E
⊢ ∀ (a : ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p), IsGalois F E

Tactic:
4 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
tfae_3_to_1 : ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E
⊢ ∀ (a : ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p), IsGalois F E

Tactic:
tfae_have 4 → 1 := fun ⟨h, hp1, _⟩ ↦ of_separable_splitting_field hp1
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
tfae_1_to_2 : ∀ (a : IsGalois F E), Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥
tfae_1_to_3 : ∀ (a : IsGalois F E), Nat.card.{u_2} Gal(E/F) = finrank F E
tfae_1_to_4 : ∀ (a : IsGalois F E), ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : ∀ (a : Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥), IsGalois F E
tfae_3_to_1 : ∀ (a : Nat.card.{u_2} Gal(E/F) = finrank F E), IsGalois F E
tfae_4_to_1 : ∀ (a : ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p), IsGalois F E
⊢ [IsGalois F E, Eq.{u_2 + 1} (α := IntermediateField F E) (fixedField ⊤) ⊥, Nat.card.{u_2} Gal(E/F) = finrank F E,
      ∃ (p : F[X]), p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
obtain : ∀ (T : F[X]) (hT₁ : T.Separable) (hT₂ : Polynomial.IsSplittingField.{u_1, u_2} F (↥K) T), IsGalois (↥L) E
⊢ IsGalois (↥L) E

Tactic:
obtain ⟨T, hT₁, hT₂⟩ := IsGalois.is_separable_splitting_field F K

Premises used: Membership.mem, Subtype, IsGalois.is_separable_splitting_field
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : Polynomial.IsSplittingField.{u_1, u_2} F (↥K) T
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
suffices : Polynomial.IsSplittingField (↥L) E T'
⊢ IsGalois (↥L) E

Tactic:
suffices T'.IsSplittingField L E from IsGalois.of_separable_splitting_field (p := T') hT₁.map
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ : Polynomial.IsSplittingField.{u_1, u_2} F (↥K) T
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
rw :
  ∀
    (hT₂ :
      Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
        Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤),
    let T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T;
    Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T') ∧
      Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
⊢ Polynomial.IsSplittingField (↥L) E T'

Tactic:
rw [isSplittingField_iff_intermediateField] at hT₂ ⊢

Premises used: isSplittingField_iff_intermediateField
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
left : Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T')
right : Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤
⊢ Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T') ∧
    Eq (α := IntermediateField (↥L) E) (adjoin (↥L) (T'.rootSet E)) ⊤

Tactic:
constructor
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
left : Polynomial.Splits (Polynomial.map (algebraMap F E) T)
⊢ Polynomial.Splits (Polynomial.map (algebraMap (↥L) E) T')

Tactic:
rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, Polynomial.map_map
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Polynomial.Splits (Polynomial.map (algebraMap F E) T)

Tactic:
Polynomial.Splits.of_algHom hT₂.1 (IsScalarTower.toAlgHom _ _ _)

Premises used: IsScalarTower.toAlgHom, Polynomial.Splits.of_algHom, And.left
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ Polynomial.Splits (Polynomial.map (algebraMap F E) T)

Tactic:
exact Polynomial.Splits.of_algHom hT₂.1 (IsScalarTower.toAlgHom _ _ _)

Premises used: IsScalarTower.toAlgHom, Polynomial.Splits.of_algHom, And.left
-- Module: Mathlib.FieldTheory.Galois.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K L : IntermediateField F E
inst_3 : IsGalois.{u_1, u_2} F ↥K
inst_4 : FiniteDimensional.{u_1, u_2} F ↥K
h : K ⊔ L = ⊤
T : F[X]
hT₁ : T.Separable
hT₂ :
  Polynomial.Splits.{u_2} (R := ↥K) (Polynomial.map (algebraMap F ↥K) T) ∧
    Eq.{u_2 + 1} (α := IntermediateField F ↥K) (adjoin F (T.rootSet ↥K)) ⊤
T' : (↥L)[X] := Polynomial.map (algebraMap F ↥L) T
⊢ T'.rootSet E = T.rootSet E

Tactic:
simp [Set.ext_iff, Polynomial.mem_rootSet', T']

Premises used: Polynomial.mem_rootSet', Set.ext_iff