{k : Type u_1} →
  {K : Type u_2} →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            (H : ClosedSubgroup Gal(K/k)) →
              [inst_4 : (↑H).Normal] → Gal(K/k) ⧸ ↑H ≃* Gal(↥(IntermediateField.fixedField ↑H)/k)