case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ (x ∈ ⋃ (q : Quotient ↑H ↑K), quotToDoset H K q) ↔ x ∈ Set.univ
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
⊢ (⋃ (q : Quotient ↑H ↑K), quotToDoset H K q) = Set.univ
ext x
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ ∃ i x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' i * y
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ (x ∈ ⋃ (q : Quotient ↑H ↑K), quotToDoset H K q) ↔ x ∈ Set.univ
simp only [Set.mem_iUnion, quotToDoset, mem_doset, SetLike.mem_coe, exists_prop, Set.mem_univ,
  iff_true_iff]
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' (mk H K x) * y
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ ∃ i x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' i * y
use mk H K x
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out' (mk H K x) = h * x * k
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' (mk H K x) * y
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x : G
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' (mk H K x) * y
obtain ⟨h, k, h3, h4, h5⟩ := mk_out'_eq_mul H K x
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out' (mk H K x) = h * x * k
⊢ x = h⁻¹ * Quotient.out' (mk H K x) * k⁻¹
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out' (mk H K x) = h * x * k
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * Quotient.out' (mk H K x) * y
refine' ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, _⟩
no goals
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.56988
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out' (mk H K x) = h * x * k
⊢ x = h⁻¹ * Quotient.out' (mk H K x) * k⁻¹
simp only [h5, Subgroup.coe_mk, ← mul_assoc, one_mul, mul_left_inv, mul_inv_cancel_right]