case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (x ∈ ⋃ (k : { x // x ∈ K }), rightCoset (↑H) (a * ↑k)) ↔ x ∈ doset a ↑H ↑K
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a : G
⊢ (⋃ (k : { x // x ∈ K }), rightCoset (↑H) (a * ↑k)) = doset a ↑H ↑K
ext x
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (x ∈ ⋃ (k : { x // x ∈ K }), rightCoset (↑H) (a * ↑k)) ↔ x ∈ doset a ↑H ↑K
simp only [mem_rightCoset_iff, exists_prop, mul_inv_rev, Set.mem_iUnion, mem_doset,
  Subgroup.mem_carrier, SetLike.mem_coe]
case h.mp
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) → ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y

case h.mpr
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
constructor
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ K }
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
case h.mp
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) → ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
rintro ⟨y, h_h⟩
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ K }
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ x = x * (↑y⁻¹ * a⁻¹) * a * ↑y
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ K }
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ ∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y
refine' ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, _⟩
no goals
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ K }
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ x = x * (↑y⁻¹ * a⁻¹) * a * ↑y
simp only [← mul_assoc, Subgroup.coe_mk, inv_mul_cancel_right, SubgroupClass.coe_inv]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ ∃ i, x✝ * ((↑i)⁻¹ * a⁻¹) ∈ H
case h.mpr
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ x_1, x_1 ∈ H ∧ ∃ y, y ∈ K ∧ x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H
rintro ⟨x, hx, y, hy, hxy⟩
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ x✝ * ((↑{ val := y, property := hy })⁻¹ * a⁻¹) ∈ H
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ ∃ i, x✝ * ((↑i)⁻¹ * a⁻¹) ∈ H
refine' ⟨⟨y, hy⟩, _⟩
no goals
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.59583
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ x✝ * ((↑{ val := y, property := hy })⁻¹ * a⁻¹) ∈ H
simp only [hxy, ← mul_assoc, hx, mul_inv_cancel_right, Subgroup.coe_mk]