∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  [FiniteDimensional F E] [IsGalois F E], Nat.card ↥K.fixingSubgroup = Module.finrank (↥K) E