∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (H : AddSubgroup α),
  s ≤ t →
    ∀ (a b : ↥H),
      (QuotientAddGroup.leftRel (s.addSubgroupOf H)) a b → (QuotientAddGroup.leftRel (t.addSubgroupOf H)) (id a) (id b)