awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ ((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
have 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
Tactic: conv_lhs => rw [← this, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).2 : G) =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) 1 h1) : G)
have 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)
Tactic: rw [equiv_snd_eq_inv_mul, equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have a₁ : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) g hg) : G)⁻¹ * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have a₂ : 1 = (↑(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]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 =
    Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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) : (a : G) → (↑S : Type u_1) × (↑T : Type u_1)) g).1 : G) =
    (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ S) 1 h1) : G)
have 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)
Tactic: rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have a₁ : g * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ T) g hg) : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have a₂ : 1 = (↑(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]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (hypothesis)
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 (α := (↑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))
have 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
Tactic: have : (hSK.equiv (g * k)).fst = (hSK.equiv g).fst :=
    hSK.equiv_fst_eq_iff_leftCosetEquivalence.2
      (by simp [LeftCosetEquivalence, leftCoset_eq_iff])
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ 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)
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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
⊢ (↑((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)
have 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)
Tactic: rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have 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)
Tactic: rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have 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)
Tactic: rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have 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)
Tactic: rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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)
⊢ (↑((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)
have 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))
Tactic: rw [coe_mul, equiv_snd_eq_inv_mul, this, equiv_snd_eq_inv_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H : Set G) T
h : ↥H
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))
have 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))
Tactic: have : (hHT.equiv (h * g)).2 = (hHT.equiv g).2 := hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
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))
⊢ 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))
have refine_1 : RightCosetEquivalence (↑H : Set G) ((↑h : G) * g) g
Tactic: have : (hHT.equiv (h * g)).2 = (hHT.equiv g).2 := hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 ?_