awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) =
    Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1)

Tactic:
congr_arg₂ (· * ·) ?_ ?_

Premises used: HMul.hMul, congr_arg₂
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
refine_2 : Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H''
refine_2₁ : Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) = Nat.card.{u_1} (↑S : Type u_1)
⊢ Nat.card.{u_1} ↥(map H.subtype H'') * Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) =
    Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1)

Tactic:
refine congr_arg₂ (· * ·) ?_ ?_

Premises used: HMul.hMul, congr_arg₂
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H''

Tactic:
Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ Nat.card.{u_1} ↥(map H.subtype H'') = Nat.card.{u_1} ↥H''

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) = Nat.card.{u_1} (↑S : Type u_1)

Tactic:
Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this_1 : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'' : Set ↥H) S
this : Nat.card.{u_1} ↥H'' * Nat.card.{u_1} (↑S : Type u_1) = Nat.card.{u_1} ↥H
⊢ Nat.card.{u_1} (↑((⇑H.subtype : (a : ↥H) → G) '' S) : Type u_1) = Nat.card.{u_1} (↑S : Type u_1)

Tactic:
exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Premises used: Equiv.Set.image, Subgroup.subtype_injective, Nat.card_congr, Equiv.symm
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
x : (↑S : Type u_1) × (↑T : Type u_1)
⊢ (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G) x = (↑x.1 : G) * (↑x.2 : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
⊢ HMul.hMul (α := G) (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G)
      (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) =
    g

Tactic:
(Equiv.ofBijective (fun x : S × T => x.1.1 * x.2.1) hST).right_inv g

Premises used: HMul.hMul, Equiv.right_inv, Prod.fst, Equiv.ofBijective, Subtype.val, Prod.snd
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) =
    g * (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹

Tactic:
eq_mul_inv_of_mul_eq (hST.equiv_fst_mul_equiv_snd g)

Premises used: eq_mul_inv_of_mul_eq, Subgroup.IsComplement.equiv_fst_mul_equiv_snd
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) =
    (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g

Tactic:
eq_inv_mul_of_mul_eq (hST.equiv_fst_mul_equiv_snd g)

Premises used: Subgroup.IsComplement.equiv_fst_mul_equiv_snd, eq_inv_mul_of_mul_eq
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
rw :
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 ↔
    g₁⁻¹ * g₂ ∈ K
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 ↔
    LeftCosetEquivalence (↑K : Set G) g₁ g₂

Tactic:
rw [LeftCosetEquivalence, leftCoset_eq_iff]

Premises used: LeftCosetEquivalence, leftCoset_eq_iff
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
mp :
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 →
    g₁⁻¹ * g₂ ∈ K
mpr :
  g₁⁻¹ * g₂ ∈ K →
    Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
      ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 ↔
    g₁⁻¹ * g₂ ∈ K

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
mp :
  (↑(HMul.hMul (α := ↥K)
          ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).2⁻¹
          ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).2) :
      G) ∈
    K
⊢ 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]

Premises used: mul_assoc, Subgroup.coe_inv, Subgroup.IsComplement.equiv_fst_mul_equiv_snd, Subgroup.coe_mul, mul_inv_rev, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
⊢ (↑(HMul.hMul (α := ↥K)
          ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).2⁻¹
          ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).2) :
      G) ∈
    K

Tactic:
Subtype.property _

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1
⊢ (↑(HMul.hMul (α := ↥K)
          ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).2⁻¹
          ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).2) :
      G) ∈
    K

Tactic:
exact Subtype.property _

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
mpr :
  (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1 : G)⁻¹ *
      g₁ ∈
    (↑K : Set G)
mpr₁ :
  (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ *
      g₁ ∈
    (↑K : Set G)
⊢ Eq.{u_1 + 1} (α := (↑S : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1

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

Premises used: Subgroup.isComplement_iff_existsUnique_inv_mul_mem, Iff.mp, ExistsUnique.unique
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
mpr :
  (g₁ *
          (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).2 :
              G)⁻¹)⁻¹ *
      g₁ ∈
    (↑K : Set G)
⊢ (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).1 : G)⁻¹ *
      g₁ ∈
    (↑K : Set G)

Tactic:
rw [equiv_fst_eq_mul_inv]

Premises used: Subgroup.IsComplement.equiv_fst_eq_mul_inv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (g₁ *
          (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₁).2 :
              G)⁻¹)⁻¹ *
      g₁ ∈
    (↑K : Set G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
mpr :
  (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ *
        g₁ *
      (g₁⁻¹ * g₂) ∈
    K
⊢ (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ *
      g₁ ∈
    (↑K : Set G)

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

Premises used: SetLike.mem_coe, mul_mem_cancel_right
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
mpr :
  (g₂ *
            (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).2 :
                G)⁻¹)⁻¹ *
        g₁ *
      (g₁⁻¹ * g₂) ∈
    K
⊢ (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).1 : G)⁻¹ *
        g₁ *
      (g₁⁻¹ * g₂) ∈
    K

Tactic:
rw [equiv_fst_eq_mul_inv]

Premises used: Subgroup.IsComplement.equiv_fst_eq_mul_inv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ K
⊢ (g₂ *
            (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g₂).2 :
                G)⁻¹)⁻¹ *
        g₁ *
      (g₁⁻¹ * g₂) ∈
    K

Tactic:
simp [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
rw :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 ↔
    g₂ * g₁⁻¹ ∈ H
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 ↔
    RightCosetEquivalence (↑H : Set G) g₁ g₂

Tactic:
rw [RightCosetEquivalence, rightCoset_eq_iff]

Premises used: rightCoset_eq_iff, RightCosetEquivalence
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
mp :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 →
    g₂ * g₁⁻¹ ∈ H
mpr :
  g₂ * g₁⁻¹ ∈ H →
    Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
      ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 ↔
    g₂ * g₁⁻¹ ∈ H

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
mp :
  (↑(HMul.hMul (α := ↥H)
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).1
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).1⁻¹) :
      G) ∈
    H
⊢ 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]

Premises used: mul_assoc, Subgroup.coe_inv, Subgroup.IsComplement.equiv_fst_mul_equiv_snd, Subgroup.coe_mul, mul_inv_rev, mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
⊢ (↑(HMul.hMul (α := ↥H)
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).1
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).1⁻¹) :
      G) ∈
    H

Tactic:
Subtype.property _

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h :
  Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2
⊢ (↑(HMul.hMul (α := ↥H)
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).1
          ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).1⁻¹) :
      G) ∈
    H

Tactic:
exact Subtype.property _

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
mpr :
  g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2 :
          G)⁻¹ ∈
    (↑H : Set G)
mpr₁ :
  g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 :
          G)⁻¹ ∈
    (↑H : Set G)
⊢ Eq.{u_1 + 1} (α := (↑T : Type u_1))
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2

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

Premises used: Iff.mp, ExistsUnique.unique, Subgroup.isComplement_iff_existsUnique_mul_inv_mem
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
mpr :
  g₁ *
      ((↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).1 :
              G)⁻¹ *
          g₁)⁻¹ ∈
    (↑H : Set G)
⊢ g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).2 :
          G)⁻¹ ∈
    (↑H : Set G)

Tactic:
rw [equiv_snd_eq_inv_mul]

Premises used: Subgroup.IsComplement.equiv_snd_eq_inv_mul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₁ *
      ((↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₁).1 :
              G)⁻¹ *
          g₁)⁻¹ ∈
    (↑H : Set G)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
mpr :
  g₂ * g₁⁻¹ *
      (g₁ *
        (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 :
            G)⁻¹) ∈
    H
⊢ g₁ *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 :
          G)⁻¹ ∈
    (↑H : Set G)

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

Premises used: SetLike.mem_coe, mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
mpr :
  g₂ *
      (g₁⁻¹ *
        (g₁ *
          ((↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).1 :
                  G)⁻¹ *
              g₂)⁻¹)) ∈
    H
⊢ g₂ * g₁⁻¹ *
      (g₁ *
        (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).2 :
            G)⁻¹) ∈
    H

Tactic:
rw [equiv_snd_eq_inv_mul, mul_assoc]

Premises used: mul_assoc, Subgroup.IsComplement.equiv_snd_eq_inv_mul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g₁ g₂ : G
h : g₂ * g₁⁻¹ ∈ H
⊢ g₂ *
      (g₁⁻¹ *
        (g₁ *
          ((↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g₂).1 :
                  G)⁻¹ *
              g₂)⁻¹)) ∈
    H

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g : G
rw :
  LeftCosetEquivalence (↑K : Set G) g
    (g *
      (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).2 : G)⁻¹)
⊢ LeftCosetEquivalence (↑K : Set G) g
    (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).1 : G)

Tactic:
rw [equiv_fst_eq_mul_inv]

Premises used: Subgroup.IsComplement.equiv_fst_eq_mul_inv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g : G
⊢ LeftCosetEquivalence (↑K : Set G) g
    (g *
      (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).2 : G)⁻¹)

Tactic:
simp [LeftCosetEquivalence, leftCoset_eq_iff]

Premises used: LeftCosetEquivalence, leftCoset_eq_iff
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g : G
rw :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g *
      g⁻¹ ∈
    H
⊢ RightCosetEquivalence (↑H : Set G) g
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 : G)

Tactic:
rw [RightCosetEquivalence, rightCoset_eq_iff, equiv_snd_eq_inv_mul]

Premises used: rightCoset_eq_iff, RightCosetEquivalence, Subgroup.IsComplement.equiv_snd_eq_inv_mul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
g : G
⊢ (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g *
      g⁻¹ ∈
    H

Tactic:
simp
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
rw :
  ({ toFun := fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G), invFun := surjInv ⋯, left_inv := ⋯,
              right_inv := ⋯ : (↑S : Type u_1) × (↑T : Type u_1) ≃ G }.symm.symm :
        (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
    g
⊢ (hST.equiv (S := S) (T := T).symm : (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
    g

Tactic:
rw [equiv, Equiv.ofBijective]

Premises used: Subgroup.IsComplement.equiv, Equiv.ofBijective
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ ({ toFun := fun (x : (↑S : Type u_1) × (↑T : Type u_1)) ↦ (↑x.1 : G) * (↑x.2 : G), invFun := surjInv ⋯, left_inv := ⋯,
              right_inv := ⋯ : (↑S : Type u_1) × (↑T : Type u_1) ≃ G }.symm.symm :
        (a : (↑S : Type u_1) × (↑T : Type u_1)) → G)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) =
    g

Tactic:
simp