Congruence_Class_Modulo_Subgroup_is_Coset

import Mathlib.Analysis.Complex.Basic

theorem Congruence_Class_Modulo_Subgroup_is_Coset {G : Type _} [Group G] (H : Subgroup G) (a b : G) (h : a⁻¹ * b ∈ H) : ∃ h₀ : G, h₀ ∈ H ∧ b = a * h₀ := by sorry