-- Mathlib/GroupTheory/DoubleCoset.lean
theorem doset_union_rightCoset (H K : Subgroup G) (a : G) :
    ⋃ k : K, op (a * k) • ↑H = doset a H K

Proof state:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ x = x * (↑y⁻¹ * a⁻¹) * a * ↑y

Tactic:
simp only [← mul_assoc, Subgroup.coe_mk, inv_mul_cancel_right, InvMemClass.coe_inv]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ x ∈ ⋃ k, op (a * ↑k) • ↑H ↔ x ∈ doset a ↑H ↑K

Tactic:
simp only [mem_rightCoset_iff, exists_prop, mul_inv_rev, Set.mem_iUnion, mem_doset,
  Subgroup.mem_carrier, SetLike.mem_coe]

Result:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Proof state:
case h.mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) → ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Tactic:
rintro ⟨y, h_h⟩

Result:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Proof state:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Tactic:
refine ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, ?_⟩

Result:
case h.mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ x = x * (↑y⁻¹ * a⁻¹) * a * ↑y

Proof state:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Tactic:
constructor

Result:
case h.mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H) → ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

case h.mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a : G
⊢ ⋃ k, op (a * ↑k) • ↑H = doset a ↑H ↑K

Tactic:
ext x

Result:
case h
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ x ∈ ⋃ k, op (a * ↑k) • ↑H ↔ x ∈ doset a ↑H ↑K

Proof state:
case h.mpr
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
⊢ (∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y) → ∃ i, x * ((↑i)⁻¹ * a⁻¹) ∈ H

Tactic:
rintro ⟨x, hx, y, hy, hxy⟩

Result:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group 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

Proof state:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ x✝ * ((↑⟨y, hy⟩)⁻¹ * a⁻¹) ∈ H

Tactic:
simp only [hxy, ← mul_assoc, hx, mul_inv_cancel_right, Subgroup.coe_mk]

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group 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

Tactic:
refine ⟨⟨y, hy⟩, ?_⟩

Result:
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x✝ x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x✝ = x * a * y
⊢ x✝ * ((↑⟨y, hy⟩)⁻¹ * a⁻¹) ∈ H