-- Mathlib/FieldTheory/Galois/Basic.lean
theorem tfae [FiniteDimensional F E] : List.TFAE [
    IsGalois F E,
    IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥,
    Fintype.card (E ≃ₐ[F] E) = finrank F E,
    ∃ p : F[X], p.Separable ∧ p.IsSplittingField F E]

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
tfae_4_to_1 : (∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p) → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_have 2 → 1 := of_fixedField_eq_bot F E

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_have 4 → 1 := fun ⟨h, hp1, _⟩ ↦ of_separable_splitting_field hp1

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
tfae_4_to_1 : (∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p) → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_have 1 → 4 := fun _ ↦ is_separable_splitting_field F E

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

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

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_have 1 → 3 := fun _ ↦ card_aut_eq_finrank F E

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE

Tactic:
tfae_have 3 → 1 := of_card_aut_eq_finrank F E

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
tfae_1_to_2 : IsGalois F E → fixedField ⊤ = ⊥
tfae_1_to_3 : IsGalois F E → Fintype.card (E ≃ₐ[F] E) = finrank F E
tfae_1_to_4 : IsGalois F E → ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p
tfae_2_to_1 : fixedField ⊤ = ⊥ → IsGalois F E
tfae_3_to_1 : Fintype.card (E ≃ₐ[F] E) = finrank F E → IsGalois F E
⊢ [IsGalois F E, fixedField ⊤ = ⊥, Fintype.card (E ≃ₐ[F] E) = finrank F E,
      ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE