awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have 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 sorry;
  ∀
    (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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have 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
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)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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 = ⊤
have refine : ∀ (g : G), Membership.mem (γ := Set G) ⊤ g → g ∈ (↑(closure U) : Set G) * R
Tactic: refine top_le_iff.mp fun g _ => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
have refine_1 : 1 ∈ (↑(closure U) : Set G) * R
Tactic: refine closure_induction_right ?_ ?_ ?_ (eq_top_iff.mp hS (mem_top g))
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ g ∈ (↑(closure U) : Set G) * R
have 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
Tactic: refine closure_induction_right ?_ ?_ ?_ (eq_top_iff.mp hS (mem_top g))
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ g ∈ (↑(closure U) : Set G) * R
have 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
Tactic: refine closure_induction_right ?_ ?_ ?_ (eq_top_iff.mp hS (mem_top g))
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ (fun (x1 x2 : G) ↦ x1 * x2) u r * s ∈ (↑(closure U) : Set G) * R
have refine_2 : u * (r * s * (↑(f (r * s)) : G)⁻¹) * (↑(f (r * s)) : G) ∈ (↑(closure U) : Set G) * R
Tactic: rw [show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group]
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
have refine_2 : Membership.mem (γ := Subgroup G) (closure U) (r * s * (↑(f (r * s)) : G)⁻¹)
Tactic: refine Set.mul_mem_mul ((closure U).mul_mem hu ?_) (f (r * s)).coe_prop
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ (fun (x1 x2 : G) ↦ x1 * x2) u r * s⁻¹ ∈ (↑(closure U) : Set G) * R
have refine_3 : u * ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)⁻¹ * (↑(f (r * s⁻¹)) : G) ∈ (↑(closure U) : Set G) * R
Tactic: rw [show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹) by group]
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
have refine_3 : Membership.mem (γ := Subgroup G) (closure U) ((↑(f (r * s⁻¹)) : G) * s * r⁻¹)
Tactic: refine Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem ?_)) (f (r * s⁻¹)).2
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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⁻¹)
have refine_3 : (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) ((↑(f (r * s⁻¹)) : G) * s) = (↑(f (r * s⁻¹)) : G) * s * r⁻¹
Tactic: refine subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ (fun (g : G) ↦ g * (↑(f g) : G)⁻¹) ((↑(f (r * s⁻¹)) : G) * s) = (↑(f (r * s⁻¹)) : G) * s * r⁻¹
have 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
Tactic: rw [mul_right_inj, inv_inj, ← Subtype.coe_mk r hr, ← Subtype.ext_iff, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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 ((↑(hR.toRightFun (T := R) ((↑(Subtype.mk (p := Membership.mem R) r hr) : G) * s⁻¹)) : G) * s) =
    Subtype.mk (p := Membership.mem R) r hr
have refine_3 : (↑(f (r * s⁻¹)) : G) * s * (↑(Subtype.mk (p := Membership.mem R) r hr) : G)⁻¹ ∈ (↑H : Set G)
Tactic: apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
      (hR.mul_inv_toRightFun_mem (f (r * s⁻¹) * s))
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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) * s * (↑(Subtype.mk (p := Membership.mem R) r hr) : G)⁻¹ ∈ (↑H : Set G)
have refine_3 : (↑(f (r * s⁻¹)) : G) * ((↑(Subtype.mk (p := Membership.mem R) r hr) : G) * s⁻¹)⁻¹ ∈ (↑H : Set G)
Tactic: rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
have rw : (fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S) ⊆ (↑H : Set G)
Tactic: rw [closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
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
have hU : 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
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
have refine : ∀ (h : G) (hh : h ∈ H),
  Membership.mem (γ := Subgroup G) (closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) h
Tactic: refine le_antisymm hU fun h hh => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Membership.mem (γ := Subgroup G) (closure ((fun (g : G) ↦ g * (↑(hR.toRightFun (T := R) g) : G)⁻¹) '' (R * S))) h
have 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)
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)
Cleared hypotheses: h, hh
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ 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)
have suffices : Subtype.mk (p := fun (x : G) ↦ x ∈ R) r hr = Subtype.mk (p := fun (x : G) ↦ x ∈ R) 1 hR1
Tactic: suffices (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R) by
    simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]