-- Mathlib/GroupTheory/Complement.lean
theorem equiv_snd_eq_iff_rightCosetEquivalence {g₁ g₂ : G} :
    (hHT.equiv g₁).snd = (hHT.equiv g₂).snd ↔ RightCosetEquivalence H g₁ g₂

Proof state:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * (↑(hHT.equiv g₂).2)⁻¹ ∈ ↑H

Tactic:
rw [SetLike.mem_coe, ← mul_mem_cancel_left h]

Result:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * g₁⁻¹ * (g₁ * (↑(hHT.equiv g₂).2)⁻¹) ∈ H

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2

Tactic:
apply (isComplement_iff_existsUnique_mul_inv_mem.1 hHT g₁).unique

Result:
case mpr.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * (↑(hHT.equiv g₁).2)⁻¹ ∈ ↑H

case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * (↑(hHT.equiv g₂).2)⁻¹ ∈ ↑H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 ↔ g₂ * g₁⁻¹ ∈ H

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 → g₂ * g₁⁻¹ ∈ H

case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ g₂ * g₁⁻¹ ∈ H → (hHT.equiv g₁).2 = (hHT.equiv g₂).2

Proof state:
case mpr.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * ((↑(hHT.equiv g₁).1)⁻¹ * g₁)⁻¹ ∈ ↑H

Tactic:
simp

Result:
no goals

Proof state:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 → g₂ * g₁⁻¹ ∈ H

Tactic:
intro h

Result:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ g₂ * g₁⁻¹ ∈ H

Proof state:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ g₂ * g₁⁻¹ ∈ H

Tactic:
rw [← hHT.equiv_fst_mul_equiv_snd g₂, ← hHT.equiv_fst_mul_equiv_snd g₁, ← h,
  mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← coe_inv, ← coe_mul]

Result:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑((hHT.equiv g₂).1 * (hHT.equiv g₁).1⁻¹) ∈ H

Proof state:
case mpr.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * (↑(hHT.equiv g₁).2)⁻¹ ∈ ↑H

Tactic:
rw [equiv_snd_eq_inv_mul]

Result:
case mpr.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ * ((↑(hHT.equiv g₁).1)⁻¹ * g₁)⁻¹ ∈ ↑H

Proof state:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * (g₁⁻¹ * (g₁ * ((↑(hHT.equiv g₂).1)⁻¹ * g₂)⁻¹)) ∈ H

Tactic:
simp

Result:
no goals

Proof state:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : (hHT.equiv g₁).2 = (hHT.equiv g₂).2
⊢ ↑((hHT.equiv g₂).1 * (hHT.equiv g₁).1⁻¹) ∈ H

Tactic:
exact Subtype.property _

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ g₂ * g₁⁻¹ ∈ H → (hHT.equiv g₁).2 = (hHT.equiv g₂).2

Tactic:
intro h

Result:
case mpr
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2

Proof state:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * g₁⁻¹ * (g₁ * (↑(hHT.equiv g₂).2)⁻¹) ∈ H

Tactic:
rw [equiv_snd_eq_inv_mul, mul_assoc]

Result:
case mpr.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ * (g₁⁻¹ * (g₁ * ((↑(hHT.equiv g₂).1)⁻¹ * g₂)⁻¹)) ∈ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 ↔ RightCosetEquivalence (↑H) g₁ g₂

Tactic:
rw [RightCosetEquivalence, rightCoset_eq_iff]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
g₁ g₂ : G
⊢ (hHT.equiv g₁).2 = (hHT.equiv g₂).2 ↔ g₂ * g₁⁻¹ ∈ H