[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
hb : b ∈ doset a ↑H ↑K
⊢ doset b ↑H ↑K = doset a ↑H ↑K
[PROOFSTEP]
obtain ⟨_, k, ⟨h, a, hh, rfl : _ = _, rfl⟩, hk, rfl⟩ := hb
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
k h a : G
hh : h ∈ ↑H
hk : k ∈ ↑K
⊢ doset ((fun x x_1 => x * x_1) ((fun x x_1 => x * x_1) h a) k) ↑H ↑K = doset a ↑H ↑K
[PROOFSTEP]
rw [doset, doset, ← Set.singleton_mul_singleton, ← Set.singleton_mul_singleton, mul_assoc, mul_assoc,
  Subgroup.singleton_mul_subgroup hk, ← mul_assoc, ← mul_assoc, Subgroup.subgroup_mul_singleton hh]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
rw [Set.not_disjoint_iff] at h 
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
simp only [mem_doset] at *
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
refine' ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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'⁻¹)
[PROOFSTEP]
rwa [mul_assoc, mul_assoc, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc, eq_mul_inv_iff_mul_eq]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset a ↑H ↑K) (doset b ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
[PROOFSTEP]
rw [disjoint_comm] at h 
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
⊢ doset a ↑H ↑K = doset b ↑H ↑K
[PROOFSTEP]
have ha : a ∈ doset b H K := mem_doset_of_not_disjoint h
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : ¬Disjoint (doset b ↑H ↑K) (doset a ↑H ↑K)
ha : a ∈ doset b ↑H ↑K
⊢ doset a ↑H ↑K = doset b ↑H ↑K
[PROOFSTEP]
apply doset_eq_of_mem ha
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Setoid.Rel (setoid ↑⊥ ↑H) = Setoid.Rel (QuotientGroup.leftRel H)
[PROOFSTEP]
ext a b
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ Setoid.Rel (setoid ↑⊥ ↑H) a b ↔ Setoid.Rel (QuotientGroup.leftRel H) a b
[PROOFSTEP]
rw [rel_iff, Setoid.Rel, QuotientGroup.leftRel_apply]
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1) → a⁻¹ * b ∈ H
[PROOFSTEP]
rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
[PROOFSTEP]
change a⁻¹ * (1 * a * b) ∈ H
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
[PROOFSTEP]
rwa [one_mul, inv_mul_cancel_left]
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ a⁻¹ * b ∈ H → ∃ a_2, a_2 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_2 * a * b_1
[PROOFSTEP]
rintro (h : a⁻¹ * b ∈ H)
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ ∃ a_1, a_1 ∈ ⊥ ∧ ∃ b_1, b_1 ∈ H ∧ b = a_1 * a * b_1
[PROOFSTEP]
exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = 1 * a * (a⁻¹ * b)
[PROOFSTEP]
rw [one_mul, mul_inv_cancel_left]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Setoid.Rel (setoid ↑H ↑⊥) = Setoid.Rel (QuotientGroup.rightRel H)
[PROOFSTEP]
ext a b
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ Setoid.Rel (setoid ↑H ↑⊥) a b ↔ Setoid.Rel (QuotientGroup.rightRel H) a b
[PROOFSTEP]
rw [rel_iff, Setoid.Rel, QuotientGroup.rightRel_apply]
[GOAL]
case h.h.a
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
[PROOFSTEP]
constructor
[GOAL]
case h.h.a.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ (∃ a_1, a_1 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_1 * a * b_1) → b * a⁻¹ ∈ H
[PROOFSTEP]
rintro ⟨b, hb, a, rfl : a = 1, rfl⟩
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b * a * 1 * a⁻¹ ∈ H
[PROOFSTEP]
change b * a * 1 * a⁻¹ ∈ H
[GOAL]
case h.h.a.mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b * a * 1 * a⁻¹ ∈ H
[PROOFSTEP]
rwa [mul_one, mul_inv_cancel_right]
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
⊢ b * a⁻¹ ∈ H → ∃ a_2, a_2 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_2 * a * b_1
[PROOFSTEP]
rintro (h : b * a⁻¹ ∈ H)
[GOAL]
case h.h.a.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ ∃ a_1, a_1 ∈ H ∧ ∃ b_1, b_1 ∈ ⊥ ∧ b = a_1 * a * b_1
[PROOFSTEP]
exact ⟨b * a⁻¹, h, 1, rfl, by rw [mul_one, inv_mul_cancel_right]⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ b = b * a⁻¹ * a * 1
[PROOFSTEP]
rw [mul_one, inv_mul_cancel_right]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
⊢ mk H K a = mk H K b ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
[PROOFSTEP]
rw [Quotient.eq'']
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
⊢ Setoid.r a b ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
[PROOFSTEP]
apply rel_iff
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
have := eq H K (mk H K g : Quotient ↑H ↑K).out' g
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K (Quotient.out' (mk H K g)) = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
rw [out_eq'] at this 
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out' (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out' (mk H K g) = h * g * k
[PROOFSTEP]
refine' ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq _)⟩
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g✝ : G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ g = h * Quotient.out' (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out' (mk H K g) * k
⊢ h * (Quotient.out' (mk H K g) * k) = g
[PROOFSTEP]
rw [← mul_assoc, ← T]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ mk H K a = mk H K b
[PROOFSTEP]
rw [eq]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : G
h : doset a ↑H ↑K = doset b ↑H ↑K
⊢ ∃ h, h ∈ H ∧ ∃ k, k ∈ K ∧ b = h * a * k
[PROOFSTEP]
exact mem_doset.mp (h.symm ▸ mem_doset_self H K b)
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
⊢ a ≠ b → Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
[PROOFSTEP]
contrapose!
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
⊢ ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K) → a = b
[PROOFSTEP]
intro h
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
a b : Quotient ↑H.toSubmonoid ↑K
h : ¬Disjoint (doset (Quotient.out' a) ↑H ↑K) (doset (Quotient.out' b) ↑H ↑K)
⊢ a = b
[PROOFSTEP]
simpa [out_eq'] using mk_eq_of_doset_eq (eq_of_not_disjoint h)
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H K : Subgroup G
⊢ ⋃ (q : Quotient ↑H ↑K), quotToDoset H K q = Set.univ
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
simp only [Set.mem_iUnion, quotToDoset, mem_doset, SetLike.mem_coe, exists_prop, Set.mem_univ, iff_true_iff]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
use mk H K x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
obtain ⟨h, k, h3, h4, h5⟩ := mk_out'_eq_mul H K x
[GOAL]
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
refine' ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, _⟩
[GOAL]
case h.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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⁻¹
[PROOFSTEP]
simp only [h5, Subgroup.coe_mk, ← mul_assoc, one_mul, mul_left_inv, mul_inv_cancel_right]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
simp only [mem_rightCoset_iff, exists_prop, mul_inv_rev, Set.mem_iUnion, mem_doset, Subgroup.mem_carrier,
  SetLike.mem_coe]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
rintro ⟨y, h_h⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
refine' ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, _⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
simp only [← mul_assoc, Subgroup.coe_mk, inv_mul_cancel_right, SubgroupClass.coe_inv]
[GOAL]
case h.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
rintro ⟨x, hx, y, hy, hxy⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
refine' ⟨⟨y, hy⟩, _⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
simp only [hxy, ← mul_assoc, hx, mul_inv_cancel_right, Subgroup.coe_mk]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
ext x
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
simp only [mem_leftCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doset]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
constructor
[GOAL]
case h.mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
rintro ⟨y, h_h⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
refine' ⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, _⟩
[GOAL]
case h.mp.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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)
[PROOFSTEP]
simp only [← mul_assoc, one_mul, mul_right_inv, mul_inv_cancel_right, SubgroupClass.coe_inv]
[GOAL]
case h.mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
rintro ⟨x, hx, y, hy, hxy⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
refine' ⟨⟨x, hx⟩, _⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type u_2
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
[PROOFSTEP]
simp only [hxy, ← mul_assoc, hy, one_mul, mul_left_inv, Subgroup.coe_mk, inv_mul_cancel_right]
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Quotient ↑⊥.toSubmonoid ↑H = (G ⧸ H)
[PROOFSTEP]
unfold Quotient
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑⊥.toSubmonoid ↑H) = (G ⧸ H)
[PROOFSTEP]
congr
[GOAL]
case e_s
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ setoid ↑⊥.toSubmonoid ↑H = QuotientGroup.leftRel H
[PROOFSTEP]
ext
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑⊥.toSubmonoid ↑H) a✝ b✝ ↔ Setoid.Rel (QuotientGroup.leftRel H) a✝ b✝
[PROOFSTEP]
simp_rw [← bot_rel_eq_leftRel H]
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑⊥.toSubmonoid ↑H) a✝ b✝ ↔ Setoid.Rel (setoid ↑⊥ ↑H) a✝ b✝
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ Quotient ↑H.toSubmonoid ↑⊥ = _root_.Quotient (QuotientGroup.rightRel H)
[PROOFSTEP]
unfold Quotient
[GOAL]
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ _root_.Quotient (setoid ↑H.toSubmonoid ↑⊥) = _root_.Quotient (QuotientGroup.rightRel H)
[PROOFSTEP]
congr
[GOAL]
case e_s
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
⊢ setoid ↑H.toSubmonoid ↑⊥ = QuotientGroup.rightRel H
[PROOFSTEP]
ext
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (QuotientGroup.rightRel H) a✝ b✝
[PROOFSTEP]
simp_rw [← rel_bot_eq_right_group_rel H]
[GOAL]
case e_s.H
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : Mul α
J : Subgroup G
g : G
H : Subgroup G
a✝ b✝ : G
⊢ Setoid.Rel (setoid ↑H.toSubmonoid ↑⊥) a✝ b✝ ↔ Setoid.Rel (setoid ↑H ↑⊥) a✝ b✝
[PROOFSTEP]
rfl
