awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ (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:
have : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g := by
    rw [equiv, Equiv.ofBijective]; 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
this :
  (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
rw : (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1).1
| ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1

Tactic:
rw [← this, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- 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
this :
  (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
conv_lhs :
  ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
conv_lhs₁ :
  (Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg

Tactic:
conv_lhs => rw [← this, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
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) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    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) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    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 ∈ S
hg : g ∈ T
⊢ ({ 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) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    g

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 ∈ S
hg : g ∈ T
⊢ (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) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    g

Tactic:
have : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g := by
    rw [equiv, Equiv.ofBijective]; 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 ∈ S
hg : g ∈ T
this :
  (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) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    g
rw : (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg).2
| ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2

Tactic:
rw [← this, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
this :
  (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) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) =
    g
conv_lhs :
  ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg
conv_lhs₁ :
  (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg).2 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg

Tactic:
conv_lhs => rw [← this, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- 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
a :
  (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) : G)
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1

Tactic:
ext
-- 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
a :
  (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G)⁻¹ * g =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) : G)
a₁ : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg) : G)⁻¹ * g = (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) : G)
a₂ a₃ : 1 = (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) : G)
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) : G)

Tactic:
rw [equiv_snd_eq_inv_mul, equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg, inv_mul_cancel]

Premises used: inv_mul_cancel, Subgroup.IsComplement.equiv_fst_eq_self_of_mem_of_one_mem, Subgroup.IsComplement.equiv_snd_eq_inv_mul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
a :
  (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1) : G)
⊢ ((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1

Tactic:
ext
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
a :
  g * (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G)⁻¹ =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1) : G)
a₁ : g * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) : G)⁻¹ = (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1) : G)
a₂ a₃ : 1 = (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1) : G)
⊢ (↑((hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1) : G)

Tactic:
rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_cancel]

Premises used: Subgroup.IsComplement.equiv_snd_eq_self_of_mem_of_one_mem, mul_inv_cancel, 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
k : ↥K
⊢ LeftCosetEquivalence (↑K : Set G) (g * (↑k : G)) 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
K : Subgroup G
S : Set G
hSK : IsComplement S (↑K : Set G)
g : G
k : ↥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 * (↑k : 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:
have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst :=
    hSK.equiv_fst_eq_iff_leftCosetEquivalence.2
      (by simp [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
k : ↥K
this :
  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 * (↑k : G))).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).1
fst :
  Eq (α := G)
    (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
            (g * (↑k : G))).1 :
      G)
    (↑(((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).2 *
              k).1 :
      G)
snd :
  (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
            (g * (↑k : G))).2 :
      G) =
    (↑(((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).2 *
              k).2 :
      G)
⊢ Eq (α := (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) (g * (↑k : G)) :
      (↑S : Type u_1) × (↑(↑K : Set G) : 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).2 * k) :
      (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))

Tactic:
ext
-- 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
k : ↥K
this :
  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 * (↑k : G))).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).1
fst fst₁ :
  Eq (α := G)
    (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).1 : G)
    (↑(((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).2 *
              k).1 :
      G)
⊢ Eq (α := G)
    (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
            (g * (↑k : G))).1 :
      G)
    (↑(((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).2 *
              k).1 :
      G)

Tactic:
rw [this]
-- 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
k : ↥K
this :
  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 * (↑k : G))).1
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) g).1
snd :
  (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
            (g * (↑k : G))).2 :
      G) =
    (↑((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)
snd₁ :
  (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
                (g * (↑k : G))).1 :
          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) *
      (↑k : G)
snd₂ :
  (↑((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 : G)) =
    (↑((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)
snd₃ :
  (↑((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 : 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 : G)
snd₄ snd₅ :
  (↑((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 : 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 : G))
⊢ (↑((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
            (g * (↑k : G))).2 :
      G) =
    (↑(((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).2 *
              k).2 :
      G)

Tactic:
rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]

Premises used: mul_assoc, Subgroup.coe_mul, Subgroup.IsComplement.equiv_snd_eq_inv_mul
-- 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 k : G
h : k ∈ K
⊢ Eq (α := (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))
    ((hSK.equiv (S := S) (T := (↑K : Set G)) : (a : G) → (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1)) (g * k) :
      (↑S : Type u_1) × (↑(↑K : Set G) : 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).2 *
          Subtype.mk (p := fun (x : G) ↦ x ∈ (↑K : Set G)) k h) :
      (↑S : Type u_1) × (↑(↑K : Set G) : Type u_1))

Tactic:
equiv_mul_right _ g ⟨k, h⟩

Premises used: Subtype.mk, Subgroup.IsComplement.equiv_mul_right
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
refine_2 :
  ∀
    (this :
      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))
            ((↑h : G) * 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 (α := (↑(↑H : Set G) : Type u_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))
          ((↑h : G) * g) :
        (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
      ((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).2) :
        ↥H × (↑T : Type u_1))
refine_1 : RightCosetEquivalence (↑H : Set G) ((↑h : G) * g) g
⊢ Eq (α := (↑(↑H : Set G) : Type u_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)) ((↑h : G) * g) :
      (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
    ((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).2) :
      ↥H × (↑T : Type u_1))

Tactic:
have : (hHT.equiv (h * g)).2 = (hHT.equiv g).2 := hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 ?_
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  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)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(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).2).1 :
      G)
refine_2₁ :
  Eq (α := G)
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).2 :
      G)
    (↑(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).2).2 :
      G)
⊢ Eq (α := (↑(↑H : Set G) : Type u_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)) ((↑h : G) * g) :
      (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
    ((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).2) :
      ↥H × (↑T : Type u_1))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  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)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 :
  (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      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)
refine_2₁ :
  (↑h : G) * g *
      (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
                ((↑h : G) * 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).1 : G)
refine_2₂ :
  (↑h : 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).1 : G)
refine_2₃ :
  (↑h : 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) *
      (g *
        (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 :
            G)⁻¹)
refine_2₄ refine_2₅ :
  (↑h : 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) *
      (g *
        (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2 :
            G)⁻¹)
⊢ (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).1 :
      G) =
    (↑(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).2).1 :
      G)

Tactic:
rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]

Premises used: mul_assoc, Subgroup.coe_mul, Subgroup.IsComplement.equiv_fst_eq_mul_inv
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
this :
  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)) ((↑h : G) * g)).2
    ((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1)) g).2
refine_2 refine_2₁ :
  Eq (α := 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 * ((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).2).2 :
      G)
⊢ Eq (α := G)
    (↑((hHT.equiv (S := (↑H : Set G)) (T := T) : (a : G) → (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
            ((↑h : G) * g)).2 :
      G)
    (↑(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).2).2 :
      G)

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
g : G
⊢ RightCosetEquivalence (↑H : Set G) ((↑h : G) * g) g

Tactic:
simp [RightCosetEquivalence, ← smul_smul]

Premises used: RightCosetEquivalence, smul_smul
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h g : G
hh : h ∈ H
⊢ Eq (α := (↑(↑H : Set G) : Type u_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)) (h * g) :
      (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))
    ((Subtype.mk (p := fun (x : G) ↦ x ∈ (↑H : Set G)) h hh *
          ((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).2) :
      (↑(↑H : Set G) : Type u_1) × (↑T : Type u_1))

Tactic:
equiv_mul_left _ ⟨h, hh⟩ g

Premises used: Set.Mem, Subtype.mk, Subgroup.IsComplement.equiv_mul_left
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
rw :
  Eq (α := G) (1 : 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) 1 hs1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 ht1) :
      G)
⊢ (hST.equiv (S := S) (T := T) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) 1 =
    (Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 hs1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 ht1)

Tactic:
rw [Equiv.apply_eq_iff_eq_symm_apply]

Premises used: Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.GroupTheory.Complement
Goal:
G : Type u_1
inst : Group G
S T : Set G
hST : IsComplement S T
hs1 : 1 ∈ S
ht1 : 1 ∈ T
⊢ Eq (α := G) (1 : 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) 1 hs1, Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 ht1) :
      G)

Tactic:
simp [equiv]

Premises used: Subgroup.IsComplement.equiv