-- Mathlib/GroupTheory/Complement.lean
theorem equiv_fst_eq_iff_leftCosetEquivalence {g₁ g₂ : G} :
    (hSK.equiv g₁).fst = (hSK.equiv g₂).fst ↔ LeftCosetEquivalence K g₁ g₂

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

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

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

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

Tactic:
exact Subtype.property _

Result:
no goals

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

Tactic:
simp [equiv_fst_eq_mul_inv, ← mul_assoc]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ LeftCosetEquivalence (↑K) g₁ g₂

Tactic:
rw [LeftCosetEquivalence, leftCoset_eq_iff]

Result:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ g₁⁻¹ * g₂ ∈ K

Proof state:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1 → g₁⁻¹ * g₂ ∈ K

Tactic:
intro h

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

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

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

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

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

Tactic:
rw [equiv_fst_eq_mul_inv]

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

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1

Tactic:
apply (isComplement_iff_existsUnique_inv_mul_mem.1 hSK g₁).unique

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

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

Proof state:
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1 ↔ g₁⁻¹ * g₂ ∈ K

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1 → g₁⁻¹ * g₂ ∈ K

case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ g₁⁻¹ * g₂ ∈ K → (hSK.equiv g₁).1 = (hSK.equiv g₂).1

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

Tactic:
rw [equiv_fst_eq_mul_inv]

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

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

Tactic:
simp

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
⊢ g₁⁻¹ * g₂ ∈ K → (hSK.equiv g₁).1 = (hSK.equiv g₂).1

Tactic:
intro h

Result:
case mpr
G : Type u_1
inst✝ : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S ↑K
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (hSK.equiv g₁).1 = (hSK.equiv g₂).1