G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ∃ x, x ∈ doset a ↑H ↑K ∧ x ∈ doset b ↑H ↑K
⊢ b ∈ doset a ↑H ↑K
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)
⊢ b ∈ doset a ↑H ↑K
rw [Set.not_disjoint_iff] at h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ∃ x, (∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y) ∧ ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * b * y
⊢ ∃ x, x ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ b = x * a * y
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ∃ x, x ∈ doset a ↑H ↑K ∧ x ∈ doset b ↑H ↑K
⊢ b ∈ doset a ↑H ↑K
simp only [mem_doset] at *
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ ∃ x, x ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ b = x * a * y
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ∃ x, (∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y) ∧ ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * b * y
⊢ ∃ x, x ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ b = x * a * y
obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ ∃ x, x ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ b = x * a * y
refine' ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), _⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.6410
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
rwa [mul_assoc, mul_assoc, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc, eq_mul_inv_iff_mul_eq]