∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h_le : s ≤ t) (f : α ⧸ t → α)
  (hf : Function.RightInverse f QuotientGroup.mk) (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t),
  (Subgroup.quotientEquivProdOfLE' h_le f hf).symm a = Quotient.map' (fun b => f a.1 * ↑b) ⋯ a.2