-- Mathlib/FieldTheory/Galois/Basic.lean
theorem card_aut_eq_finrank [FiniteDimensional F E] [IsGalois F E] :
    Fintype.card (E ≃ₐ[F] E) = finrank F E

Proof state:
case intro.f.right_inv
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
ϕ : ↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯
⊢ (fun ϕ => iso.trans (ϕ.trans iso.symm)) ((fun ϕ => iso.symm.trans (ϕ.trans iso)) ϕ) = ϕ

Tactic:
ext1

Result:
case intro.f.right_inv.h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
ϕ : ↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯
a✝ : ↥F⟮α⟯
⊢ ((fun ϕ => iso.trans (ϕ.trans iso.symm)) ((fun ϕ => iso.symm.trans (ϕ.trans iso)) ϕ)) a✝ = ϕ a✝

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
e : E
⊢ e ∈ F⟮α⟯

Tactic:
rw [hα]

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
e : E
⊢ e ∈ ⊤

Proof state:
case intro.f.left_inv.h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
ϕ : E ≃ₐ[F] E
a✝ : E
⊢ ((fun ϕ => iso.symm.trans (ϕ.trans iso)) ((fun ϕ => iso.trans (ϕ.trans iso.symm)) ϕ)) a✝ = ϕ a✝

Tactic:
simp only [trans_apply, apply_symm_apply]

Result:
no goals

Proof state:
case intro.f.right_inv.h
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
iso : ↥F⟮α⟯ ≃ₐ[F] E :=
  { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯,
    commutes' := ⋯ }
H : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
ϕ : ↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯
a✝ : ↥F⟮α⟯
⊢ ((fun ϕ => iso.trans (ϕ.trans iso.symm)) ((fun ϕ => iso.symm.trans (ϕ.trans iso)) ϕ)) a✝ = ϕ a✝

Tactic:
simp only [trans_apply, symm_apply_apply]

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
inst✝ : IsGalois F E
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E

Tactic:
obtain ⟨α, hα⟩ := Field.exists_primitive_element F E

Result:
case intro
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
α : E
hα : F⟮α⟯ = ⊤
⊢ Fintype.card (E ≃ₐ[F] E) = finrank F E