G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
have := eq H K (mk H K g : Quotient ↑H ↑K).out' g
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
rw [out_eq'] at this
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
refine' ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq _)⟩
no goals
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
α : Type ?u.30227
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
rw [← mul_assoc, ← T]