awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1)
h : Nat.card.{u_1} ↥(_root_.commutator G) = 0
⊢ index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1) =
    0

Tactic:
rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2

Premises used: zero_dvd_iff, card_commutator_closureCommutatorRepresentatives
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h2 :
  Nat.card.{u_1} ↥(_root_.commutator ↥(closureCommutatorRepresentatives G)) ∣
    index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1)
h : Nat.card.{u_1} ↥(_root_.commutator G) = 0
h2₁ :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1) =
    0
⊢ Nat.card.{u_1} ↥(_root_.commutator G) = 0

Tactic:
rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2

Premises used: zero_dvd_iff, card_commutator_closureCommutatorRepresentatives
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h2 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1) =
    0
h : Nat.card.{u_1} ↥(_root_.commutator G) = 0
⊢ False

Tactic:
FiniteIndex.index_ne_zero (eq_zero_of_pow_eq_zero h2)

Premises used: Subgroup.FiniteIndex.index_ne_zero, eq_zero_of_pow_eq_zero
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
h2 :
  index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) ^
      (index.{u_1} (G := ↥(closureCommutatorRepresentatives G)) (center ↥(closureCommutatorRepresentatives G)) *
          Nat.card.{u_1} (↑(commutatorSet ↥(closureCommutatorRepresentatives G)) : Type u_1) +
        1) =
    0
h : Nat.card.{u_1} ↥(_root_.commutator G) = 0
⊢ False

Tactic:
exact FiniteIndex.index_ne_zero (eq_zero_of_pow_eq_zero h2)

Premises used: Subgroup.FiniteIndex.index_ne_zero, eq_zero_of_pow_eq_zero
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
rw : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y)⁻¹ 1
rw₁ : Eq.{u_1 + 1} (α := ↥H) 1⁻¹ 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := ↥H) 1 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) y x) 1

Tactic:
rw [← diff_inv, h, inv_one]

Premises used: inv_one, Subgroup.leftTransversals.diff_inv
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β x y z : H.LeftTransversal
h : Eq (α := ↥H) (diff (MonoidHom.id ↥H) x y) 1
h' : Eq (α := ↥H) (diff (MonoidHom.id ↥H) y z) 1
rw : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) x y) (diff (MonoidHom.id ↥H) y z) = 1
S : H.LeftTransversal
rw₁ : HMul.hMul (α := ↥H) 1 (diff (MonoidHom.id ↥H) y z) = 1
rw₂ : HMul.hMul (α := ↥H) 1 1 = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := ↥H) 1 1
⊢ Eq (α := ↥H) (diff (MonoidHom.id ↥H) x z) 1

Tactic:
rw [← diff_mul_diff, h, h', one_mul]

Premises used: Subgroup.leftTransversals.diff_mul_diff, one_mul
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
rw : (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯) : G) = (↑1 : G)
rw₁ : (unop g)⁻¹ * (↑1 : G) * unop g = (↑1 : G)
rw₂ : (unop g)⁻¹ * 1 * unop g = 1
rw₃ : (unop g)⁻¹ * unop g = 1
rw₄ rw₅ : Eq.{u_1 + 1} (α := G) 1 1
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑1 : G) * unop g) ⋯ = 1

Tactic:
rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]

Premises used: inv_mul_cancel, Subgroup.coe_mk, Subtype.ext_iff, Subgroup.coe_one, mul_one
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
h₁ h₂ : ↥H
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑(h₁ * h₂) : G) * unop g) ⋯ =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑h₁ : G) * unop g) ⋯ *
      Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑h₂ : G) * unop g) ⋯

Tactic:
simp only [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]

Premises used: mul_assoc, Subtype.ext_iff, Subgroup.coe_mul, mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H :=
  { toFun := fun (h : ↥H) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑h : G) * unop g) ⋯, map_one' := ⋯,
    map_mul' := ⋯ }
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑(diff (MonoidHom.id ↥H) α β) : G) * unop g) ⋯

Tactic:
(Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm

Premises used: Fintype.prod_equiv, Subgroup.leftTransversals.diff, MulAction.toPerm, map_prod, Equiv.symm, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H :=
  { toFun := fun (h : ↥H) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑h : G) * unop g) ⋯, map_one' := ⋯,
    map_mul' := ⋯ }
refine :
  ∀ (x : G ⧸ H),
    Eq (α := ↥H)
      ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑(g • α) : Set G)) : (a : G ⧸ H) → (↑(↑(g • α) : Set G) : Type u_1)) x) :
                  G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑(g • β) : Set G)) : (a : G ⧸ H) → (↑(↑(g • β) : Set G) : Type u_1)) x) :
                G))
            ⋯) :
        ↥H)
      ((ϕ : (a : ↥H) → ↥H)
          ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              (HMul.hMul (α := G)
                (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1))
                        ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x)) :
                    G)⁻¹
                (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1))
                      ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x)) :
                  G))
              ⋯)) :
        ↥H)
⊢ diff (MonoidHom.id ↥H) (g • α) (g • β) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑(diff (MonoidHom.id ↥H) α β) : G) * unop g) ⋯

Tactic:
refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm

Premises used: Fintype.prod_equiv, MulAction.toPerm, map_prod, Equiv.symm, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
hH : H.Normal
g : Gᵐᵒᵖ
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
ϕ : ↥H →* ↥H :=
  { toFun := fun (h : ↥H) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((unop g)⁻¹ * (↑h : G) * unop g) ⋯, map_one' := ⋯,
    map_mul' := ⋯ }
x : G ⧸ H
⊢ Eq (α := ↥H)
    ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑(g • α) : Set G)) : (a : G ⧸ H) → (↑(↑(g • α) : Set G) : Type u_1)) x) :
                G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(g • β) : Set G)) : (a : G ⧸ H) → (↑(↑(g • β) : Set G) : Type u_1)) x) : G))
          ⋯) :
      ↥H)
    ((ϕ : (a : ↥H) → ↥H)
        ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1))
                      ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x)) :
                  G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1))
                    ((Equiv.symm (toPerm g) : (a : G ⧸ H) → G ⧸ H) x)) :
                G))
            ⋯)) :
      ↥H)

Tactic:
simp only [ϕ, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc,
    MonoidHom.id_apply, toPerm_symm_apply, MonoidHom.coe_mk, OneHom.coe_mk]

Premises used: mul_assoc, OneHom.coe_mk, MulAction.toPerm_symm_apply, Subgroup.smul_apply_eq_smul_apply_inv_smul, MonoidHom.coe_mk, MonoidHom.id_apply, mul_inv_rev, MulOpposite.smul_eq_mul_unop
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
rw :
  Eq.{u_1 + 1} (α := H.LeftTransversal) ((fun (α : H.LeftTransversal) ↦ op (g₂⁻¹ * g₁⁻¹) • α) T)
    ((fun (α : H.LeftTransversal) ↦ op g₁⁻¹ • α) ((fun (α : H.LeftTransversal) ↦ op g₂⁻¹ • α) T))
⊢ Eq.{u_1 + 1} (α := H.LeftTransversal) ((fun (α : H.LeftTransversal) ↦ op (g₁ * g₂)⁻¹ • α) T)
    ((fun (α : H.LeftTransversal) ↦ op g₁⁻¹ • α) ((fun (α : H.LeftTransversal) ↦ op g₂⁻¹ • α) T))

Tactic:
rw [mul_inv_rev]

Premises used: mul_inv_rev
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ Eq.{u_1 + 1} (α := H.LeftTransversal) ((fun (α : H.LeftTransversal) ↦ op (g₂⁻¹ * g₁⁻¹) • α) T)
    ((fun (α : H.LeftTransversal) ↦ op g₁⁻¹ • α) ((fun (α : H.LeftTransversal) ↦ op g₂⁻¹ • α) T))

Tactic:
mul_smul (op g₁⁻¹) (op g₂⁻¹) T

Premises used: Inv.inv, MulOpposite.unop, SemigroupAction.mul_smul, MulOpposite.op
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
g₁ g₂ : G
q : H.QuotientDiff
T : H.LeftTransversal
⊢ Eq.{u_1 + 1} (α := H.LeftTransversal) ((fun (α : H.LeftTransversal) ↦ op (g₂⁻¹ * g₁⁻¹) • α) T)
    ((fun (α : H.LeftTransversal) ↦ op g₁⁻¹ • α) ((fun (α : H.LeftTransversal) ↦ op g₂⁻¹ • α) T))

Tactic:
exact mul_smul (op g₁⁻¹) (op g₂⁻¹) T

Premises used: Inv.inv, SemigroupAction.mul_smul, MulOpposite.op
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
q : H.QuotientDiff
T : H.LeftTransversal
rw : (fun (α : H.LeftTransversal) ↦ HSMul.hSMul (α := Gᵐᵒᵖ) (op 1) α) T = T
⊢ (fun (α : H.LeftTransversal) ↦ HSMul.hSMul (α := Gᵐᵒᵖ) (op 1⁻¹) α) T = T

Tactic:
rw [inv_one]

Premises used: inv_one
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
q : H.QuotientDiff
T : H.LeftTransversal
⊢ (fun (α : H.LeftTransversal) ↦ HSMul.hSMul (α := Gᵐᵒᵖ) (op 1) α) T = T

Tactic:
apply one_smul Gᵐᵒᵖ T

Premises used: MulOpposite, one_smul
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
rw :
  Eq.{u_1 + 1} (α := ↥H)
    (∏ q : G ⧸ H,
      (MonoidHom.id ↥H : (a : ↥H) → ↥H)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                  q) :
              G))
          ⋯))
    (∏ x : G ⧸ H,
      HMul.hMul (α := ↥H)
        ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              (HMul.hMul (α := G)
                (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) x) : G)⁻¹
                (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) x) : G))
              ⋯) :
          ↥H)
        h)
⊢ diff (MonoidHom.id ↥H) α (op (↑h : G) • β) = diff (MonoidHom.id ↥H) α β * h ^ H.index

Tactic:
rw [diff, diff, index_eq_card, Nat.card_eq_fintype_card,
      ← Finset.card_univ, ← Finset.prod_const, ← Finset.prod_mul_distrib]

Premises used: Finset.card_univ, Finset.prod_mul_distrib, Subgroup.leftTransversals.diff, Finset.prod_const, Subgroup.index_eq_card, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
⊢ Eq.{u_1 + 1} (α := ↥H)
    (∏ q : G ⧸ H,
      (MonoidHom.id ↥H : (a : ↥H) → ↥H)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                  q) :
              G))
          ⋯))
    (∏ x : G ⧸ H,
      HMul.hMul (α := ↥H)
        ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              (HMul.hMul (α := G)
                (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) x) : G)⁻¹
                (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) x) : G))
              ⋯) :
          ↥H)
        h)

Tactic:
Finset.prod_congr rfl fun q _ => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
refine :
  ∀ (q : G ⧸ H),
    Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q →
      (MonoidHom.id ↥H : (a : ↥H) → ↥H)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                      (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                    q) :
                G))
            ⋯) =
        HMul.hMul (α := ↥H)
          ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
              (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
                (HMul.hMul (α := G)
                  (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
                  (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G))
                ⋯) :
            ↥H)
          h
⊢ Eq.{u_1 + 1} (α := ↥H)
    (∏ q : G ⧸ H,
      (MonoidHom.id ↥H : (a : ↥H) → ↥H)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
          (HMul.hMul (α := G)
            (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
            (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                    (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                  q) :
              G))
          ⋯))
    (∏ x : G ⧸ H,
      HMul.hMul (α := ↥H)
        ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
              (HMul.hMul (α := G)
                (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) x) : G)⁻¹
                (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) x) : G))
              ⋯) :
          ↥H)
        h)

Tactic:
refine Finset.prod_congr rfl fun q _ => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
h_1 : Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q
simp_rw :
  (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
            (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
          q) :
      G) =
    (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G) * (↑h : G)
⊢ (MonoidHom.id ↥H : (a : ↥H) → ↥H)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        (HMul.hMul (α := G)
          (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
                  (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
                q) :
            G))
        ⋯) =
    HMul.hMul (α := ↥H)
      ((MonoidHom.id ↥H : (a : ↥H) → ↥H)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑α : Set G)) : (a : G ⧸ H) → (↑(↑α : Set G) : Type u_1)) q) : G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G))
            ⋯) :
        ↥H)
      h

Tactic:
simp_rw [Subtype.ext_iff, MonoidHom.id_apply, coe_mul, mul_assoc, mul_right_inj]

Premises used: mul_assoc, Subtype.ext_iff, Subgroup.coe_mul, mul_right_inj, MonoidHom.id_apply
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
h_1 : Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q
rw : q = op (↑h : G) • q
⊢ (↑((⋯.leftQuotientEquiv (S := (↑(op (↑h : G) • β) : Set G)) :
            (a : G ⧸ H) → (↑(↑(op (↑h : G) • β) : Set G) : Type u_1))
          q) :
      G) =
    (↑((⋯.leftQuotientEquiv (S := (↑β : Set G)) : (a : G ⧸ H) → (↑(↑β : Set G) : Type u_1)) q) : G) * (↑h : G)

Tactic:
rw [smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, MulOpposite.unop_op, mul_left_inj,
    ← Subtype.ext_iff, Equiv.apply_eq_iff_eq, inv_smul_eq_iff]

Premises used: inv_smul_eq_iff, mul_left_inj, Subgroup.smul_apply_eq_smul_apply_inv_smul, Subtype.ext_iff, MulOpposite.unop_op, MulOpposite.smul_eq_mul_unop, Equiv.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
h_1 : Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q
⊢ q = op (↑h : G) • q

Tactic:
left_eq_mul.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)

Premises used: Iff.mpr, left_eq_mul, Quotient, Quot.map, Quotient.map', MulOpposite.unop, QuotientGroup.eq_one_iff, Subtype.property
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
α β : H.LeftTransversal
inst_3 : H.Normal
h : ↥H
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
q : G ⧸ H
h_1 : Membership.mem (γ := Finset (G ⧸ H)) Finset.univ q
⊢ q = op (↑h : G) • q

Tactic:
exact left_eq_mul.mpr ((QuotientGroup.eq_one_iff _).mpr h.2)

Premises used: Iff.mpr, left_eq_mul, QuotientGroup.eq_one_iff, Subtype.property
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : HSMul.hSMul (β := H.QuotientDiff) h (Quotient.mk'' α) = Quotient.mk'' α
rw : h ^ H.index = (diff (MonoidHom.id ↥H) α (op (↑h⁻¹ : G) • α))⁻¹
rw₁ : h ^ H.index = (diff (MonoidHom.id ↥H) α α * h⁻¹ ^ H.index)⁻¹
rw₂ : h ^ H.index = (1 * h⁻¹ ^ H.index)⁻¹
rw₃ : h ^ H.index = (h⁻¹ ^ H.index)⁻¹
rw₄ : h ^ H.index = (h ^ H.index)⁻¹⁻¹
rw₅ rw₆ : h ^ H.index = h ^ H.index
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op (↑h⁻¹ : G) • α) α

Tactic:
rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]

Premises used: Subgroup.leftTransversals.diff_self, inv_pow, inv_inv, Subgroup.leftTransversals.diff_inv, Subgroup.smul_diff', one_mul
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
α_1 β_1 : H.QuotientDiff
β α : H.LeftTransversal
rw :
  diff (MonoidHom.id ↥H) β α *
      (HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)) H.index)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := ↥H) (β := ↥H) (diff (MonoidHom.id ↥H) β α : ↥H)
      (((powCoprime hH : (a : ↥H) → ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α)))⁻¹ : ↥H) =
    1
rw₂ : HMul.hMul (α := ↥H) (diff (MonoidHom.id ↥H) β α) (diff (MonoidHom.id ↥H) β α)⁻¹ = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := ↥H) 1 1
⊢ diff (MonoidHom.id ↥H) β α *
      HPow.hPow (α := ↥H) (((powCoprime hH).symm : (a : ↥H) → ↥H) (diff (MonoidHom.id ↥H) β α))⁻¹ H.index =
    1

Tactic:
rw [inv_pow, ← powCoprime_apply hH, Equiv.apply_symm_apply, mul_inv_cancel]

Premises used: Equiv.apply_symm_apply, inv_pow, powCoprime_apply, mul_inv_cancel
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
α : H.QuotientDiff
hH : (Nat.card.{u_1} ↥H).Coprime H.index
⊢ H.IsComplement' (stabilizer G α)

Tactic:
isComplement'_stabilizer α (eq_one_of_smul_eq_one hH α) fun g => exists_smul_eq hH (g • α) α

Premises used: Subgroup.eq_one_of_smul_eq_one, Subgroup.exists_smul_eq, Subgroup.isComplement'_stabilizer, HSMul.hSMul