-- Mathlib/FieldTheory/Galois/Basic.lean
theorem fixedField_fixingSubgroup [FiniteDimensional F E] [h : IsGalois F E] :
    IntermediateField.fixedField (IntermediateField.fixingSubgroup K) = K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ fixedField K.fixingSubgroup = K

Tactic:
suffices
  finrank K E = finrank (IntermediateField.fixedField (IntermediateField.fixingSubgroup K)) E by
  exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E

Tactic:
classical
rw [IntermediateField.finrank_fixedField_eq_card,
  Fintype.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
exact (card_aut_eq_finrank K E).symm

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = Fintype.card (E ≃ₐ[↥K] E)

Tactic:
exact (card_aut_eq_finrank K E).symm

Result:
no goals

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
⊢ fixedField K.fixingSubgroup = K

Tactic:
have K_le : K ≤ IntermediateField.fixedField (IntermediateField.fixingSubgroup K) :=
  (IntermediateField.le_iff_le _ _).mpr le_rfl

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ fixedField K.fixingSubgroup = K

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E

Tactic:
rw [IntermediateField.finrank_fixedField_eq_card,
  Fintype.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
⊢ finrank (↥K) E = Fintype.card (E ≃ₐ[↥K] E)

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
K : IntermediateField F E
inst✝ : FiniteDimensional F E
h : IsGalois F E
K_le : K ≤ fixedField K.fixingSubgroup
this : finrank (↥K) E = finrank (↥(fixedField K.fixingSubgroup)) E
⊢ fixedField K.fixingSubgroup = K

Tactic:
exact (IntermediateField.eq_of_le_of_finrank_eq' K_le this).symm

Result:
no goals