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
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
hU : closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G)
r : G
hr : r ∈ R
hh : (fun (x1 x2 : G) ↦ x1 * x2) g r ∈ H
py₁ : r * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ R) r hr) : G)⁻¹ ∈ (↑H : Set G)
py₂ : r * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ R) 1 hR1) : G)⁻¹ ∈ (↑H : Set G)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ R) r hr = Subtype.mk (p := fun (x : G) ↦ x ∈ R) 1 hR1

Tactic:
apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR r).unique

Premises used: Iff.mp, ExistsUnique.unique, Subgroup.isComplement_iff_existsUnique_mul_inv_mem
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
hU : closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G)
r : G
hr : r ∈ R
hh : (fun (x1 x2 : G) ↦ x1 * x2) g r ∈ H
py₁ : 1 ∈ (↑H : Set G)
⊢ r * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ R) r hr) : G)⁻¹ ∈ (↑H : Set G)

Tactic:
rw [Subtype.coe_mk, mul_inv_cancel]

Premises used: Subtype.coe_mk, mul_inv_cancel
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
hU : closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G)
r : G
hr : r ∈ R
hh : (fun (x1 x2 : G) ↦ x1 * x2) g r ∈ H
⊢ 1 ∈ (↑H : Set G)

Tactic:
H.one_mem

Premises used: Set.Mem, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
hU : closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G)
r : G
hr : r ∈ R
hh : (fun (x1 x2 : G) ↦ x1 * x2) g r ∈ H
⊢ 1 ∈ (↑H : Set G)

Tactic:
exact H.one_mem

Premises used: Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
hU : closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G)
r : G
hr : r ∈ R
hh : (fun (x1 x2 : G) ↦ x1 * x2) g r ∈ H
py₂ : r ∈ (↑H : Set G)
⊢ r * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ R) 1 hR1) : G)⁻¹ ∈ (↑H : Set G)

Tactic:
rw [Subtype.coe_mk, inv_one, mul_one]

Premises used: Subtype.coe_mk, inv_one, mul_one
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
hU : closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G)
r : G
hr : r ∈ R
hh : (fun (x1 x2 : G) ↦ x1 * x2) g r ∈ H
⊢ r ∈ (↑H : Set G)

Tactic:
(H.mul_mem_cancel_left (hU hg)).mp hh

Premises used: Subgroup.mul_mem_cancel_left, Iff.mp
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
hU : closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H
g : G
hg : g ∈ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G)
r : G
hr : r ∈ R
hh : (fun (x1 x2 : G) ↦ x1 * x2) g r ∈ H
⊢ r ∈ (↑H : Set G)

Tactic:
exact (H.mul_mem_cancel_left (hU hg)).mp hh

Premises used: Subgroup.mul_mem_cancel_left, Iff.mp
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
rw :
  map H.subtype ⊤ ≤
    closure
      ((fun (x : G) ↦
          (H.subtype : (a : ↥H) → G)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (x * (↑(hR.toRightFun (T := R) x) : G)⁻¹) ⋯)) ''
        (R * S))
⊢ Eq (α := Subgroup ↥H)
    (closure
      ((fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) ⋯) '' (R * S)))
    ⊤

Tactic:
rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image]

Premises used: Set.image_image, eq_top_iff, Subgroup.map_subtype_le_map_subtype, MonoidHom.map_closure
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
⊢ map H.subtype ⊤ ≤
    closure
      ((fun (x : G) ↦
          (H.subtype : (a : ↥H) → G)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (x * (↑(hR.toRightFun (T := R) x) : G)⁻¹) ⋯)) ''
        (R * S))

Tactic:
(map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))

Premises used: Set.Mem, ge_of_eq, Subgroup.closure_mul_image_eq, Subgroup.map_subtype_le, LE.le.trans, Top.top
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H : Set G) R
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure S) ⊤
⊢ map H.subtype ⊤ ≤
    closure
      ((fun (x : G) ↦
          (H.subtype : (a : ↥H) → G)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ H) (x * (↑(hR.toRightFun (T := R) x) : G)⁻¹) ⋯)) ''
        (R * S))

Tactic:
exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))

Premises used: ge_of_eq, Subgroup.closure_mul_image_eq, Subgroup.map_subtype_le, LE.le.trans, Top.top
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : DecidableEq G
R S : Finset G
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
rw :
  Eq (α := Subgroup ↥H)
    (closure
      ((fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := (↑R : Set G)) g) : G)⁻¹) ⋯) ''
        ((↑R : Set G) * (↑S : Set G))))
    ⊤
⊢ Eq (α := Subgroup ↥H)
    (closure
      (↑(Finset.image
            (fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := (↑R : Set G)) g) : G)⁻¹) ⋯)
            (R * S)) :
        Set ↥H))
    ⊤

Tactic:
rw [Finset.coe_image, Finset.coe_mul]

Premises used: Finset.coe_mul, Finset.coe_image
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : DecidableEq G
R S : Finset G
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
⊢ Eq (α := Subgroup ↥H)
    (closure
      ((fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := (↑R : Set G)) g) : G)⁻¹) ⋯) ''
        ((↑R : Set G) * (↑S : Set G))))
    ⊤

Tactic:
closure_mul_image_eq_top hR hR1 hS

Premises used: Subgroup.closure_mul_image_eq_top
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : DecidableEq G
R S : Finset G
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
⊢ Eq (α := Subgroup ↥H)
    (closure
      ((fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := (↑R : Set G)) g) : G)⁻¹) ⋯) ''
        ((↑R : Set G) * (↑S : Set G))))
    ⊤

Tactic:
exact closure_mul_image_eq_top hR hR1 hS

Premises used: Subgroup.closure_mul_image_eq_top
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
haveI : ∀ (this : DecidableEq G), ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤

Tactic:
haveI : DecidableEq G := Classical.decEq G
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this : DecidableEq G
obtain :
  ∀ (R₀ : Set G) (hR : IsComplement (↑H : Set G) R₀) (hR1 : 1 ∈ R₀),
    ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤

Tactic:
obtain ⟨R₀, hR, hR1⟩ := H.exists_isComplement_right 1

Premises used: OfNat.ofNat, Subgroup.exists_isComplement_right
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H : Set G) R₀
hR1 : 1 ∈ R₀
haveI :
  ∀ (this : Fintype (↑R₀ : Type u_1)),
    ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤

Tactic:
haveI : Fintype R₀ := Fintype.ofEquiv _ hR.rightQuotientEquiv
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H : Set G) R₀
hR1 : 1 ∈ R₀
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
rwa rwa₁ rwa₂ rwa₃ : IsComplement (↑H : Set G) R₀
⊢ IsComplement (↑H : Set G) (↑R : Set G)

Tactic:
rwa [Set.coe_toFinset]

Premises used: Set.coe_toFinset
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H : Set G) R₀
hR1 : 1 ∈ R₀
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
⊢ IsComplement (↑H : Set G) (↑R : Set G)

Tactic:
replace hR : IsComplement (H : Set G) R := by rwa [Set.coe_toFinset]
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
rwa rwa₁ rwa₂ rwa₃ : 1 ∈ R₀
⊢ 1 ∈ R

Tactic:
rwa [Set.mem_toFinset]

Premises used: Set.mem_toFinset
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
⊢ 1 ∈ R

Tactic:
replace hR1 : (1 : G) ∈ R := by rwa [Set.mem_toFinset]
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
⊢ ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤

Tactic:
⟨_, ?_, closure_mul_image_eq_top' hR hR1 hS⟩

Premises used: And.intro, Exists.intro, Subgroup.closure_mul_image_eq_top'
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
refine :
  Finset.card (α := ↥H)
      (Finset.image
        (fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := (↑R : Set G)) g) : G)⁻¹) ⋯)
        (R * S)) ≤
    H.index * #S
⊢ ∃ (T : Finset ↥H), #T ≤ H.index * #S ∧ Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤

Tactic:
refine ⟨_, ?_, closure_mul_image_eq_top' hR hR1 hS⟩
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
⊢ Finset.card (α := ↥H)
      (Finset.image
        (fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := (↑R : Set G)) g) : G)⁻¹) ⋯)
        (R * S)) ≤
    #(R * S)

Tactic:
Finset.card_image_le

Premises used: Finset.card_image_le
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
⊢ #(R * S) ≤ #R * #S

Tactic:
Finset.card_mul_le

Premises used: Finset.card_mul_le
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
⊢ #R * #S = H.index * #S

Tactic:
congr_arg (· * S.card) ?_

Premises used: HMul.hMul, congr_arg, Finset.card
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
_ : #R = H.index
⊢ Finset.card (α := ↥H)
      (Finset.image
        (fun (g : G) ↦ Subtype.mk (p := fun (x : G) ↦ x ∈ H) (g * (↑(hR.toRightFun (T := (↑R : Set G)) g) : G)⁻¹) ⋯)
        (R * S)) ≤
    H.index * #S

Tactic:
calc
    _ ≤ #(R * S) := Finset.card_image_le
    _ ≤ #R * #S := Finset.card_mul_le
    _ = H.index * S.card := congr_arg (· * S.card) ?_

Premises used: HMul.hMul, congr_arg, Finset.card_image_le, Finset.card_mul_le, Subgroup.index, Finset.card
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
⊢ #R = Fintype.card.{u_1} ↥R

Tactic:
(Fintype.card_coe R).symm

Premises used: Eq.symm, Fintype.card_coe
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
⊢ Fintype.card.{u_1} ↥R = Fintype.card.{u_1} (Quotient (QuotientGroup.rightRel H))

Tactic:
(Fintype.card_congr hR.rightQuotientEquiv).symm

Premises used: Fintype.card_congr, Subgroup.IsComplement.rightQuotientEquiv, Eq.symm
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
⊢ Fintype.card.{u_1} (Quotient (QuotientGroup.rightRel H)) = Fintype.card.{u_1} (G ⧸ H)

Tactic:
QuotientGroup.card_quotient_rightRel H

Premises used: QuotientGroup.card_quotient_rightRel
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
rw : Fintype.card.{u_1} (G ⧸ H) = Nat.card.{u_1} (G ⧸ H)
rw₁ rw₂ : Fintype.card.{u_1} (G ⧸ H) = Fintype.card.{u_1} (G ⧸ H)
⊢ Fintype.card.{u_1} (G ⧸ H) = H.index

Tactic:
rw [index_eq_card, Nat.card_eq_fintype_card]

Premises used: Subgroup.index_eq_card, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
this_1 : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this_2 : DecidableEq G
R₀ : Set G
this : Fintype (↑R₀ : Type u_1)
R : Finset G := R₀.toFinset
hR : IsComplement (↑H : Set G) (↑R : Set G)
hR1 : 1 ∈ R
R₁ : Fintype.card.{u_1} (G ⧸ H) = H.index
⊢ #R = H.index

Tactic:
calc
    #R = Fintype.card R := (Fintype.card_coe R).symm
    _ = _ := (Fintype.card_congr hR.rightQuotientEquiv).symm
    _ = Fintype.card (G ⧸ H) := QuotientGroup.card_quotient_rightRel H
    _ = H.index := by rw [index_eq_card, Nat.card_eq_fintype_card]

Premises used: Fintype.card_congr, QuotientGroup.card_quotient_rightRel, Membership.mem, Fintype.card, Subtype, HasQuotient.Quotient, Subgroup.index, Subgroup.IsComplement.rightQuotientEquiv, Eq.symm, Fintype.card_coe
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst_1 : H.FiniteIndex
obtain : ∀ (S : Finset G) (hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤), Group.FG.{u_1} ↥H
⊢ Group.FG.{u_1} ↥H

Tactic:
obtain ⟨S, hS⟩ := hG.1

Premises used: Group.FG.out
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S_1 : Set G
hG : Group.FG G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
obtain : ∀ (T : Finset ↥H) (hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤), Group.FG.{u_1} ↥H
⊢ Group.FG.{u_1} ↥H

Tactic:
obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS

Premises used: Subgroup.exists_finset_card_le_mul
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S_1 : Set G
hG : Group.FG G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
T : Finset ↥H
hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ Group.FG.{u_1} ↥H

Tactic:
⟨⟨T, hT⟩⟩

Premises used: Group.FG.mk, Exists.intro
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
R S_1 : Set G
hG : Group.FG G
inst_1 : H.FiniteIndex
S : Finset G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
T : Finset ↥H
hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ Group.FG.{u_1} ↥H

Tactic:
exact ⟨⟨T, hT⟩⟩
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.FG G
inst_1 : H.FiniteIndex
⊢ Group.FG.{u_1} ↥H

Tactic:
haveI := H.fg_of_index_ne_zero
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.FG G
inst_1 : H.FiniteIndex
this : Group.FG.{u_1} ↥H
obtain :
  ∀ (S : Finset G) (hS₀ : #S = Group.rank G) (hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤),
    Group.rank.{u_1} ↥H ≤ H.index * Group.rank G
⊢ Group.rank.{u_1} ↥H ≤ H.index * Group.rank G

Tactic:
obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G

Premises used: Group.rank_spec
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.FG G
inst_1 : H.FiniteIndex
this : Group.FG.{u_1} ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
obtain :
  ∀ (T : Finset ↥H) (hT₀ : #T ≤ H.index * #S) (hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤),
    Group.rank.{u_1} ↥H ≤ H.index * Group.rank G
⊢ Group.rank.{u_1} ↥H ≤ H.index * Group.rank G

Tactic:
obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS

Premises used: Subgroup.exists_finset_card_le_mul
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.FG G
inst_1 : H.FiniteIndex
this : Group.FG.{u_1} ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
T : Finset ↥H
hT₀ : #T ≤ H.index * #S
hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ Group.rank.{u_1} ↥H ≤ #T

Tactic:
Group.rank_le hT

Premises used: Group.rank_le
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.FG G
inst_1 : H.FiniteIndex
this : Group.FG.{u_1} ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
T : Finset ↥H
hT₀ : #T ≤ H.index * #S
hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ #T ≤ H.index * #S

Tactic:
hT₀
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.FG G
inst_1 : H.FiniteIndex
this : Group.FG.{u_1} ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
T : Finset ↥H
hT₀ : #T ≤ H.index * #S
hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ H.index * #S = H.index * Group.rank G

Tactic:
congr_arg (H.index * ·) hS₀

Premises used: HMul.hMul, congr_arg, Subgroup.index
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : Group.FG G
inst_1 : H.FiniteIndex
this : Group.FG.{u_1} ↥H
S : Finset G
hS₀ : #S = Group.rank G
hS : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
T : Finset ↥H
hT₀ : #T ≤ H.index * #S
hT : Eq (α := Subgroup ↥H) (closure (↑T : Set ↥H)) ⊤
⊢ Group.rank.{u_1} ↥H ≤ H.index * Group.rank G

Tactic:
calc
    Group.rank H ≤ #T := Group.rank_le hT
    _ ≤ H.index * #S := hT₀
    _ = H.index * Group.rank G := congr_arg (H.index * ·) hS₀

Premises used: HMul.hMul, Group.rank_le, Membership.mem, Subtype, congr_arg, Subgroup.index, Group.rank
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite.{u_1 + 1} (↑(commutatorSet G) : Type u_1)
pos :
  ∀ (hG : index (center G) = 0),
    Nat.card.{u_1} ↥(_root_.commutator G) ∣
      index (center G) ^ (index (center G) * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + 1)
neg :
  ∀ (hG : ¬index (center G) = 0),
    Nat.card.{u_1} ↥(_root_.commutator G) ∣
      index (center G) ^ (index (center G) * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + 1)
⊢ Nat.card.{u_1} ↥(_root_.commutator G) ∣
    index (center G) ^ (index (center G) * Nat.card.{u_1} (↑(commutatorSet G) : Type u_1) + 1)

Tactic:
by_cases hG : (center G).index = 0

Premises used: Subgroup.center, Subgroup.index