QuotientGroup.lift_comp

Stream: Is there code for X?

[Kim Morrison]

Where is

import Mathlib

variable {G H M : Type*} [Group G] [Group H] [Group M] (N : Subgroup G) [nN : N.Normal]

theorem QuotientGroup.lift_comp (φ : G →* H) (HN : N ≤ φ.ker) (ψ : H →* M) :
    QuotientGroup.lift (ψ.comp φ) (N := N) sorry = ψ.comp (QuotientGroup.lift φ (N := N) HN) :=
  QuotientGroup.monoidHom_ext N rfl

?
(and further, where is the sorry, which I'd have thought we'd have as a single step from HN?)

(This seems like the missing step for dealing with the erw in docs#AddCommGrp.Colimits.Quot.ι_desc.)

[Thomas Browning]

This fills the sorry: HN.trans (Subgroup.comap_mono (bot_le (a := ψ.ker))), but seems like we should add an ker_le_ker_comp lemma.