case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (x ∈ ⋃ (h : { x // x ∈ H }), leftCoset (↑h * a) ↑K) ↔ x ∈ doset a ↑H ↑K
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a : G
⊢ (⋃ (h : { x // x ∈ H }), leftCoset (↑h * a) ↑K) = doset a ↑H ↑K
ext x
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) ↔ ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (x ∈ ⋃ (h : { x // x ∈ H }), leftCoset (↑h * a) ↑K) ↔ x ∈ doset a ↑H ↑K
simp only [mem_leftCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doset]
case h.mp
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) → ∃ 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.64712
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, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K
case h
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) ↔ ∃ 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.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ H }
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ ∃ 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.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
⊢ (∃ i, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K) → ∃ 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.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ H }
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ x = ↑y * a * (a⁻¹ * ↑y⁻¹ * x)
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ H }
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ ∃ x_1, x_1 ∈ ↑H ∧ ∃ y, y ∈ ↑K ∧ x = x_1 * a * y
refine' ⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, _⟩
no goals
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a x : G
y : { x // x ∈ H }
h_h : a⁻¹ * (↑y)⁻¹ * x ∈ ↑K
⊢ x = ↑y * a * (a⁻¹ * ↑y⁻¹ * x)
simp only [← mul_assoc, one_mul, mul_right_inv, mul_inv_cancel_right, SubgroupClass.coe_inv]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
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, a⁻¹ * (↑i)⁻¹ * x✝ ∈ ↑K
case h.mpr
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
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, a⁻¹ * (↑i)⁻¹ * x ∈ ↑K
rintro ⟨x, hx, y, hy, hxy⟩
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
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
⊢ a⁻¹ * (↑{ val := x, property := hx })⁻¹ * x✝ ∈ ↑K
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
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, a⁻¹ * (↑i)⁻¹ * x✝ ∈ ↑K
refine' ⟨⟨x, hx⟩, _⟩
no goals
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.64712
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
⊢ a⁻¹ * (↑{ val := x, property := hx })⁻¹ * x✝ ∈ ↑K
simp only [hxy, ← mul_assoc, hy, one_mul, mul_left_inv, Subgroup.coe_mk, inv_mul_cancel_right]