{F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] →
              [inst_4 : Algebra F K] → (self : IntermediateField.Lifts F E K) → ↥self.carrier →ₐ[F] K