∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (a₁ a₂ : ↥s),
  Quotient.map' ⇑(AddSubgroup.inclusion h) ⋯ (Quotient.mk'' a₁) =
      Quotient.map' ⇑(AddSubgroup.inclusion h) ⋯ (Quotient.mk'' a₂) →
    Quotient.mk'' a₁ = Quotient.mk'' a₂