∀ {k : Type u_2} {K : Type u_1} {L : Type u_3} {E : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra k K] [inst_4 : Algebra k L] [inst_5 : EquivLike E K L] [inst_6 : AlgEquivClass E k K L] (e : E),
  (NumberField.RingOfIntegers.mapAlgHom (↑e).symm).comp (NumberField.RingOfIntegers.mapAlgHom e) =
    AlgHom.id (NumberField.RingOfIntegers k) (NumberField.RingOfIntegers K)