awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
obtain :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤),
    Nat.card G ∣ Monoid.exponent G ^ Group.rank G
obtain₁ :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤),
    Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
obtain₂ :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤),
    Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
obtain₃ :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤),
    let f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯;
    ∀
      (hf :
        Function.Surjective (α := (g : ↥S) → ↥(zpowers (↑g : G))) (β := G)
          (⇑f : (a : (g : ↥S) → ↥(zpowers (↑g : G))) → G)),
      Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
obtain₄ :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤)
    (hf : Nat.card G ∣ Nat.card.{u_1} ((g : ↥S) → ↥(zpowers (↑g : G)))), Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
obtain₅ :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤)
    (hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))), Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
obtain₆ :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤)
    (hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))) (g : ↥S),
    Membership.mem (γ := Finset ↥S) Finset.univ g → Nat.card.{u_1} ↥(zpowers (↑g : G)) ∣ Monoid.exponent G
obtain₇ :
  ∀ (S : Finset G) (hS1 : #S = Group.rank G) (hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤)
    (hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))) (g : ↥S),
    Membership.mem (γ := Finset ↥S) Finset.univ g → orderOf (↑g : G) ∣ Monoid.exponent G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

Tactic:
classical
  obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
  rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
  let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _
  have hf : Function.Surjective f := by
    rw [← MonoidHom.range_eq_top, eq_top_iff, ← hS2, closure_le]
    exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
  replace hf := card_dvd_of_surjective f hf
  rw [Nat.card_pi] at hf
  refine hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)
  rw [Nat.card_zpowers]
  exact Monoid.order_dvd_exponent (g : G)

Premises used: Finset.card_univ, Group.rank_spec, Finset.prod_const, Nat.card_zpowers, Nat.card_pi, Fintype.card_coe
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
n : ℕ
hG : ∀ (g : G), g ^ n = 1
⊢ Nat.card G ∣ n ^ Group.rank G

Tactic:
(card_dvd_exponent_pow_rank G).trans
    (pow_dvd_pow_of_dvd (Monoid.exponent_dvd_of_forall_pow_eq_one hG) (Group.rank G))

Premises used: card_dvd_exponent_pow_rank, pow_dvd_pow_of_dvd, Monoid.exponent_dvd_of_forall_pow_eq_one, Group.rank, Dvd.dvd.trans
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
change : (↑(closure U) : Set G) * R = ⊤
⊢ (↑(closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) : Set G) * R = ⊤

Tactic:
change (closure U : Set G) * R = ⊤

Premises used: Subgroup.closure, SetLike.coe
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
⊢ (↑(closure U) : Set G) * R = ⊤

Tactic:
top_le_iff.mp fun g _ => ?_

Premises used: top_le_iff, 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
refine : ∀ (g : G), Membership.mem (γ := Set G) ⊤ g → g ∈ (↑(closure U) : Set G) * R
⊢ (↑(closure U) : Set G) * R = ⊤

Tactic:
refine top_le_iff.mp fun g _ => ?_

Premises used: top_le_iff, 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
⊢ g ∈ (↑(closure U) : Set G) * R

Tactic:
closure_induction_right ?_ ?_ ?_ (eq_top_iff.mp hS (mem_top g))

Premises used: Subgroup.closure_induction_right, eq_top_iff, Iff.mp, Subgroup.mem_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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
refine_1 : 1 ∈ (↑(closure U) : Set G) * R
refine_2 :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure S) x) (y : G) (hy : y ∈ S),
    x ∈ (↑(closure U) : Set G) * R → x * y ∈ (↑(closure U) : Set G) * R
refine_3 :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure S) x) (y : G) (hy : y ∈ S),
    x ∈ (↑(closure U) : Set G) * R → x * y⁻¹ ∈ (↑(closure U) : Set G) * R
⊢ g ∈ (↑(closure U) : Set G) * R

Tactic:
refine closure_induction_right ?_ ?_ ?_ (eq_top_iff.mp hS (mem_top g))
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
⊢ 1 ∈ (↑(closure U) : Set G) * R

Tactic:
⟨1, (closure U).one_mem, 1, hR1, one_mul 1⟩

Premises used: Subgroup.closure, Set.Mem, setOf, Subgroup.one_mem, Set.image2, And.intro, Exists.intro, OfNat.ofNat, one_mul
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
⊢ 1 ∈ (↑(closure U) : Set G) * R

Tactic:
exact ⟨1, (closure U).one_mem, 1, hR1, one_mul 1⟩
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ u * r * s = u * (r * s * (↑(f (r * s)) : G)⁻¹) * (↑(f (r * s)) : G)

Tactic:
group
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_2 : u * (r * s * (↑(f (r * s)) : G)⁻¹) * (↑(f (r * s)) : G) ∈ (↑(closure U) : Set G) * R
⊢ (fun (x1 x2 : G) ↦ x1 * x2) u r * s ∈ (↑(closure U) : Set G) * R

Tactic:
rw [show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group]
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ u * (r * s * (↑(f (r * s)) : G)⁻¹) * (↑(f (r * s)) : G) ∈ (↑(closure U) : Set G) * R

Tactic:
Set.mul_mem_mul ((closure U).mul_mem hu ?_) (f (r * s)).coe_prop

Premises used: Subtype.coe_prop, HMul.hMul, Subgroup.closure, Subgroup.mul_mem, Set.mul_mem_mul
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_2 : Membership.mem (γ := Subgroup G) (closure U) (r * s * (↑(f (r * s)) : G)⁻¹)
⊢ u * (r * s * (↑(f (r * s)) : G)⁻¹) * (↑(f (r * s)) : G) ∈ (↑(closure U) : Set G) * R

Tactic:
refine Set.mul_mem_mul ((closure U).mul_mem hu ?_) (f (r * s)).coe_prop

Premises used: Subtype.coe_prop, HMul.hMul, Subgroup.closure, Subgroup.mul_mem, Set.mul_mem_mul
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ Membership.mem (γ := Subgroup G) (closure U) (r * s * (↑(f (r * s)) : G)⁻¹)

Tactic:
subset_closure ⟨r * s, Set.mul_mem_mul hr hs, rfl⟩

Premises used: HMul.hMul, Subgroup.subset_closure, And.intro, Exists.intro, Set.mul_mem_mul, rfl
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ Membership.mem (γ := Subgroup G) (closure U) (r * s * (↑(f (r * s)) : G)⁻¹)

Tactic:
exact subset_closure ⟨r * s, Set.mul_mem_mul hr hs, rfl⟩
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ u * r * s⁻¹ = u * ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)⁻¹ * (↑(f (r * s⁻¹)) : G)

Tactic:
group
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_3 : u * ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)⁻¹ * (↑(f (r * s⁻¹)) : G) ∈ (↑(closure U) : Set G) * R
⊢ (fun (x1 x2 : G) ↦ x1 * x2) u r * s⁻¹ ∈ (↑(closure U) : Set G) * R

Tactic:
rw [show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹) by group]
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ u * ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)⁻¹ * (↑(f (r * s⁻¹)) : G) ∈ (↑(closure U) : Set G) * R

Tactic:
Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem ?_)) (f (r * s⁻¹)).2

Premises used: HMul.hMul, Subgroup.closure, Inv.inv, Subgroup.inv_mem, Subgroup.mul_mem, Set.mul_mem_mul, Subtype.property
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_3 : Membership.mem (γ := Subgroup G) (closure U) ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)
⊢ u * ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)⁻¹ * (↑(f (r * s⁻¹)) : G) ∈ (↑(closure U) : Set G) * R

Tactic:
refine Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem ?_)) (f (r * s⁻¹)).2

Premises used: HMul.hMul, Subgroup.closure, Inv.inv, Subgroup.inv_mem, Subgroup.mul_mem, Set.mul_mem_mul, Subtype.property
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ Membership.mem (γ := Subgroup G) (closure U) ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)

Tactic:
subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, ?_⟩

Premises used: HMul.hMul, Subgroup.subset_closure, Inv.inv, And.intro, Exists.intro, Subtype.val, Set.mul_mem_mul, Subtype.property
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_3 : (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) ((↑(f (r * s⁻¹)) : G) * s) = (↑(f (r * s⁻¹)) : G) * s * r⁻¹
⊢ Membership.mem (γ := Subgroup G) (closure U) ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)

Tactic:
refine subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, ?_⟩
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_3 :
  f ((↑(hR.toRightFun (T := R) ((↑(Subtype.mk (p := Membership.mem R) r hr) : G) * s⁻¹)) : G) * s) =
    Subtype.mk (p := Membership.mem R) r hr
⊢ (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) ((↑(f (r * s⁻¹)) : G) * s) = (↑(f (r * s⁻¹)) : G) * s * r⁻¹

Tactic:
rw [mul_right_inj, inv_inj, ← Subtype.coe_mk r hr, ← Subtype.ext_iff, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Subtype.ext_iff, mul_right_inj, inv_inj
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_3 : (↑(f (r * s⁻¹)) : G) * s * (↑(Subtype.mk (p := Membership.mem R) r hr) : G)⁻¹ ∈ (↑H : Set G)
⊢ f ((↑(hR.toRightFun (T := R) ((↑(Subtype.mk (p := Membership.mem R) r hr) : G) * s⁻¹)) : G) * s) =
    Subtype.mk (p := Membership.mem R) r hr

Tactic:
apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
      (hR.mul_inv_toRightFun_mem (f (r * s⁻¹) * s))

Premises used: HMul.hMul, Subgroup.IsComplement.mul_inv_toRightFun_mem, Inv.inv, Iff.mp, ExistsUnique.unique, Subgroup.isComplement_iff_existsUnique_mul_inv_mem, Subtype.val
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
refine_3 : (↑(f (r * s⁻¹)) : G) * ((↑(Subtype.mk (p := Membership.mem R) r hr) : G) * s⁻¹)⁻¹ ∈ (↑H : Set G)
⊢ (↑(f (r * s⁻¹)) : G) * s * (↑(Subtype.mk (p := Membership.mem R) r hr) : G)⁻¹ ∈ (↑H : Set G)

Tactic:
rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]

Premises used: mul_assoc, inv_inv, mul_inv_rev
-- 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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ (↑(f (r * s⁻¹)) : G) * ((↑(Subtype.mk (p := Membership.mem R) r hr) : G) * s⁻¹)⁻¹ ∈ (↑H : Set G)

Tactic:
hR.toRightFun_mul_inv_mem (r * s⁻¹)

Premises used: HMul.hMul, Set.Mem, Inv.inv, Subgroup.IsComplement.toRightFun_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) ⊤
f : G → (↑R : Type u_1) := hR.toRightFun (T := R)
U : Set G := (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) '' (R * S)
g : G
h : Membership.mem (γ := Set G) ⊤ g
s : G
hs : s ∈ S
u : G
hu : u ∈ (↑(closure U) : Set G)
r : G
hr : r ∈ R
⊢ (↑(f (r * s⁻¹)) : G) * ((↑(Subtype.mk (p := Membership.mem R) r hr) : G) * s⁻¹)⁻¹ ∈ (↑H : Set G)

Tactic:
exact hR.toRightFun_mul_inv_mem (r * s⁻¹)

Premises used: HMul.hMul, Inv.inv, Subgroup.IsComplement.toRightFun_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) ⊤
rw : (fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S) ⊆ (↑H : Set G)
⊢ closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H

Tactic:
rw [closure_le]

Premises used: Subgroup.closure_le
-- 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) ⊤
g : G
⊢ (fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) g ∈ (↑H : Set G)

Tactic:
hR.mul_inv_toRightFun_mem g

Premises used: Set.Mem, Subgroup.IsComplement.mul_inv_toRightFun_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) ⊤
g : G
⊢ (fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) g ∈ (↑H : Set G)

Tactic:
exact hR.mul_inv_toRightFun_mem g

Premises used: Subgroup.IsComplement.mul_inv_toRightFun_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) ⊤
⊢ closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) ≤ H

Tactic:
have hU : closure ((R * S).image fun g => g * (hR.toRightFun g : G)⁻¹) ≤ H := by
    rw [closure_le]
    rintro - ⟨g, -, rfl⟩
    exact hR.mul_inv_toRightFun_mem g
-- 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
⊢ closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) = H

Tactic:
le_antisymm hU fun h hh => ?_

Premises used: le_antisymm
-- 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
refine :
  ∀ (h : G) (hh : h ∈ H),
    Membership.mem (γ := Subgroup G) (closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) h
⊢ closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)) = H

Tactic:
refine le_antisymm hU fun h hh => ?_

Premises used: le_antisymm
-- 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
h : G
hh : h ∈ H
obtain :
  ∀ (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),
    Membership.mem (γ := Subgroup G) (closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)))
      ((fun (x1 x2 : G) ↦ x1 * x2) g r)
⊢ Membership.mem (γ := Subgroup G) (closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) h

Tactic:
obtain ⟨g, hg, r, hr, rfl⟩ :=
    show h ∈ _ from eq_top_iff.mp (closure_mul_image_mul_eq_top hR hR1 hS) (mem_top h)

Premises used: eq_top_iff, Subgroup.closure_mul_image_mul_eq_top, Iff.mp, Subgroup.mem_top, rfl
-- 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
this : Subtype.mk (p := fun (x : G) ↦ x ∈ R) r hr = Subtype.mk (p := fun (x : G) ↦ x ∈ R) 1 hR1
⊢ Membership.mem (γ := Subgroup G) (closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)))
    ((fun (x1 x2 : G) ↦ x1 * x2) g r)

Tactic:
simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]

Premises used: Subtype.ext_iff, Iff.mp, 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
suffices : Subtype.mk (p := fun (x : G) ↦ x ∈ R) r hr = Subtype.mk (p := fun (x : G) ↦ x ∈ R) 1 hR1
⊢ Membership.mem (γ := Subgroup G) (closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S)))
    ((fun (x1 x2 : G) ↦ x1 * x2) g r)

Tactic:
suffices (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R) by
    simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]