awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G_1 : Type u
n_1 : ℕ
inst_2 : Group G_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst_3 : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst_4 : Group G
inst_5 : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : Equiv.{u_3 + 1, u_4 + 1} α (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : MonoidHom.{u_4, u_3} (IteratedWreathProduct G n) (Equiv.Perm α) :=
  e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf :
  Function.Injective.{u_4 + 1, u_3 + 1} (α := IteratedWreathProduct G n) (β := Equiv.Perm α)
    (⇑f : (a : IteratedWreathProduct G n) → Equiv.Perm α)
g : MulEquiv.{u_3, u_4} (↥f.range) (IteratedWreathProduct G n) := (MonoidHom.ofInjective hf).symm
rw :
  Nat.card.{u_4} (IteratedWreathProduct G n) =
    HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
rw₁ :
  HPow.hPow (β := ℕ) (Nat.card G) (∑ i ∈ Finset.range n, Nat.card G ^ i) =
    HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
rw₂ :
  HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) =
    HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
rw₃ :
  HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) =
    HPow.hPow (β := ℕ) p (((Nat.card α).factorial.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₄ :
  HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) =
    HPow.hPow (β := ℕ) p (((p ^ n).factorial.factorization : (a : ℕ) → ℕ) p : ℕ)
rw₅ : HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) = p ^ multiplicity p (p ^ n).factorial
rw₆ rw₇ : HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) = HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i)
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
rw [Nat.card_congr g.toEquiv, IteratedWreathProduct.card, hG, Nat.card_perm, hα,
        ← Nat.multiplicity_eq_factorization hp.out (p ^ n).factorial_ne_zero,
        Nat.Prime.multiplicity_factorial_pow hp.out]

Premises used: Nat.multiplicity_eq_factorization, IteratedWreathProduct.card, Nat.card_perm, MulEquiv.toEquiv, Nat.card_congr, Nat.factorial_ne_zero, HPow.hPow, Nat.Prime.multiplicity_factorial_pow, Fact.out
-- Module: Mathlib.GroupTheory.RegularWreathProduct
Goal:
D : Type u_1
Q : Type u_2
inst : Group D
inst_1 : Group Q
G_1 : Type u
n_1 : ℕ
inst_2 : Group G_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
α : Type u_3
inst_3 : Finite α
hα : Nat.card α = p ^ n
G : Type u_4
inst_4 : Group G
inst_5 : Finite G
hG : Nat.card G = p
P : Sylow p (Equiv.Perm α)
e1 : Equiv.{u_3 + 1, u_4 + 1} α (Fin n → G) := (Finite.equivFinOfCardEq hα).trans (Finite.equivFinOfCardEq ⋯).symm
f : MonoidHom.{u_4, u_3} (IteratedWreathProduct G n) (Equiv.Perm α) :=
  e1.symm.permCongrHom.toMonoidHom.comp (iteratedWreathToPermHom G n)
hf :
  Function.Injective.{u_4 + 1, u_3 + 1} (α := IteratedWreathProduct G n) (β := Equiv.Perm α)
    (⇑f : (a : IteratedWreathProduct G n) → Equiv.Perm α)
g : MulEquiv.{u_3, u_4} (↥f.range) (IteratedWreathProduct G n) := (MonoidHom.ofInjective hf).symm
P' : Sylow p (Equiv.Perm α) := ofCard f.range ⋯
⊢ MulEquiv.{u_3, u_4} (↥(↑P : Subgroup (Equiv.Perm α))) (IteratedWreathProduct G n)

Tactic:
exact (P.equiv P').trans g

Premises used: MulEquiv.trans, Sylow.equiv
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
⊢ ResiduallyFinite G ↔ Eq.{u_1 + 1} (α := Subgroup G) (⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup) ⊥

Tactic:
⟨fun h ↦ h.iInf_eq_bot, fun h ↦ ⟨h⟩⟩

Premises used: Group.ResiduallyFinite.iInf_eq_bot, Group.ResiduallyFinite.mk, Iff.intro
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
simp_rw :
  Eq.{u_1 + 1} (α := Subgroup G) (⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup) ⊥ ↔
    ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
simp_rw₁ :
  (∀ (x : G), Membership.mem (γ := Subgroup G) (⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup) x → x = 1) ↔
    ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
simp_rw₂ :
  (∀ (x : G), (∀ (i : FiniteIndexNormalSubgroup G), x ∈ i.toSubgroup) → x = 1) ↔
    ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1

Tactic:
simp_rw [residuallyFinite_def, Subgroup.eq_bot_iff_forall, Subgroup.mem_iInf,
    FiniteIndexNormalSubgroup.mem_toSubgroup_iff]

Premises used: FiniteIndexNormalSubgroup.mem_toSubgroup_iff, Subgroup.mem_iInf, Group.residuallyFinite_def, Subgroup.eq_bot_iff_forall
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
inst_1 : ResiduallyFinite G
g : G
hg : ∀ (H : FiniteIndexNormalSubgroup G), g ∈ H
⊢ g = 1

Tactic:
residuallyFinite_iff_forall_finiteIndexNormalSubgroup.mp ‹_› g hg

Premises used: Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup, Iff.mp
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
simp_rw :
  (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
    ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H
simp_rw₁ :
  (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
    ∀ (g : G), g ≠ 1 → ¬∀ (x : FiniteIndexNormalSubgroup G), g ∈ x
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H

Tactic:
simp_rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup, ← not_forall, not_imp_not]

Premises used: Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup, Classical.not_forall, not_imp_not
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
inst_1 : ResiduallyFinite G
g : G
hg : g ≠ 1
⊢ ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H

Tactic:
residuallyFinite_iff_exists_finiteIndexNormalSubgroup.mp ‹_› g hg

Premises used: Iff.mp, Group.residuallyFinite_iff_exists_finiteIndexNormalSubgroup
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
rw :
  (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
    ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1

Tactic:
rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup]

Premises used: Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
⊢ (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
    ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1

Tactic:
forall_congr' fun g ↦ ⟨fun h hg ↦ h fun H ↦ hg H,
    fun h hg ↦ h fun H hH ↦ H.normalCore_le (hg (.ofSubgroup H.normalCore))⟩

Premises used: FiniteIndexNormalSubgroup.ofSubgroup, FiniteIndexNormalSubgroup.toSubgroup, Iff.intro, forall_congr', Subgroup.normalCore, Subgroup.normalCore_le
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
⊢ (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
    ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1

Tactic:
exact forall_congr' fun g ↦ ⟨fun h hg ↦ h fun H ↦ hg H,
    fun h hg ↦ h fun H hH ↦ H.normalCore_le (hg (.ofSubgroup H.normalCore))⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
simp_rw :
  (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔
    ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
simp_rw₁ :
  (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔
    ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), ¬(H.FiniteIndex → g ∈ H)
simp_rw₂ :
  (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔
    ∀ (g : G), g ≠ 1 → ¬∀ (x : Subgroup G), x.FiniteIndex → g ∈ x
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H

Tactic:
simp_rw [residuallyFinite_iff_forall_finiteIndex, ← Classical.not_imp, ← not_forall,
    not_imp_not]

Premises used: Group.residuallyFinite_iff_forall_finiteIndex, Classical.not_imp, Classical.not_forall, not_imp_not
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
inst_1 : ResiduallyFinite G
g h : G
hgh : g ≠ h
obtain :
  ∀ (H : FiniteIndexNormalSubgroup G) (hH : g⁻¹ * h ∉ H),
    ∃ (H : FiniteIndexNormalSubgroup G), Ne (α := G ⧸ H.toSubgroup) (↑g : G ⧸ H.toSubgroup) (↑h : G ⧸ H.toSubgroup)
⊢ ∃ (H : FiniteIndexNormalSubgroup G), Ne (α := G ⧸ H.toSubgroup) (↑g : G ⧸ H.toSubgroup) (↑h : G ⧸ H.toSubgroup)

Tactic:
obtain ⟨H, hH⟩ :=
    exists_finiteIndexNormalSubgroup_notMem (g⁻¹ * h) fun h ↦ hgh <| eq_of_inv_mul_eq_one h

Premises used: HMul.hMul, eq_of_inv_mul_eq_one, Inv.inv, Group.exists_finiteIndexNormalSubgroup_notMem
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
inst_1 : ResiduallyFinite G
g h : G
hgh : g ≠ h
H : FiniteIndexNormalSubgroup G
hH : g⁻¹ * h ∉ H
⊢ Ne (α := G ⧸ H.toSubgroup) (↑g : G ⧸ H.toSubgroup) (↑h : G ⧸ H.toSubgroup)

Tactic:
simpa [QuotientGroup.eq]

Premises used: QuotientGroup.eq
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
inst_1 : ResiduallyFinite G
g h : G
hgh : g ≠ h
H : FiniteIndexNormalSubgroup G
hH : g⁻¹ * h ∉ H
⊢ ∃ (H : FiniteIndexNormalSubgroup G), Ne (α := G ⧸ H.toSubgroup) (↑g : G ⧸ H.toSubgroup) (↑h : G ⧸ H.toSubgroup)

Tactic:
exact ⟨H, by simpa [QuotientGroup.eq]⟩
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
h :
  ∀ (g : G),
    g ≠ 1 →
      ∃ (H : Type u) (x : Group H) (_ : Finite H) (f : G →* H), Ne.{u + 1} (α := H) ((f : (a : G) → H) g : H) (1 : H)
rw : ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
⊢ ResiduallyFinite G

Tactic:
rw [residuallyFinite_iff_exists_finiteIndex]

Premises used: Group.residuallyFinite_iff_exists_finiteIndex
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
h :
  ∀ (g : G),
    g ≠ 1 →
      ∃ (H : Type u) (x : Group H) (_ : Finite H) (f : G →* H), Ne.{u + 1} (α := H) ((f : (a : G) → H) g : H) (1 : H)
g : G
hg : g ≠ 1
obtain :
  ∀ (w : Type u) (w_1 : Group w),
    Finite w →
      ∀ (f : G →* w) (hf : Ne.{u + 1} (α := w) ((f : (a : G) → w) g : w) (1 : w)),
        ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
⊢ ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H

Tactic:
obtain ⟨_, _, _, f, hf⟩ := h g hg
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
h :
  ∀ (g : G),
    g ≠ 1 →
      ∃ (H : Type u) (x : Group H) (_ : Finite H) (f : G →* H), Ne.{u + 1} (α := H) ((f : (a : G) → H) g : H) (1 : H)
g : G
hg : g ≠ 1
w : Type u
w_1 : Group w
w_2 : Finite w
f : G →* w
hf : Ne.{u + 1} (α := w) ((f : (a : G) → w) g : w) (1 : w)
⊢ g ∉ f.ker

Tactic:
simpa using hf
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
inst : Group G
h :
  ∀ (g : G),
    g ≠ 1 →
      ∃ (H : Type u) (x : Group H) (_ : Finite H) (f : G →* H), Ne.{u + 1} (α := H) ((f : (a : G) → H) g : H) (1 : H)
g : G
hg : g ≠ 1
w : Type u
w_1 : Group w
w_2 : Finite w
f : G →* w
hf : Ne.{u + 1} (α := w) ((f : (a : G) → w) g : w) (1 : w)
⊢ ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H

Tactic:
exact ⟨f.ker, Subgroup.finiteIndex_ker f, by simpa using hf⟩
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : Finite G
⊢ ResiduallyFinite G

Tactic:
residuallyFinite_iff_forall_finiteIndex.mpr fun _ hg ↦ hg ⊥

Premises used: Iff.mpr, Group.residuallyFinite_iff_forall_finiteIndex, Bot.bot
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
H : Subgroup G
rw : ∀ (g : ↥H), (∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1) → g = 1
⊢ ResiduallyFinite.{u_1} ↥H

Tactic:
rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup]

Premises used: Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
H : Subgroup G
g : ↥H
hg : ∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1
a : (↑g : G) = (↑1 : G)
⊢ g = 1

Tactic:
ext
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
H : Subgroup G
g : ↥H
hg : ∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1
⊢ (↑g : G) = (↑1 : G)

Tactic:
eq_one_iff_forall_finiteIndexNormalSubroup g.1 fun K ↦ hg (K.comap H.subtype)

Premises used: Subgroup.subtype, Group.eq_one_iff_forall_finiteIndexNormalSubroup, FiniteIndexNormalSubgroup.comap, Subtype.val
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
H : Subgroup G
g : ↥H
hg : ∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1
⊢ (↑g : G) = (↑1 : G)

Tactic:
exact eq_one_iff_forall_finiteIndexNormalSubroup g.1 fun K ↦ hg (K.comap H.subtype)

Premises used: Subgroup.subtype, Group.eq_one_iff_forall_finiteIndexNormalSubroup, FiniteIndexNormalSubgroup.comap, Subtype.val
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
inst_3 : ResiduallyFinite G'
rw : ∀ (g : G × G'), (∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H) → g = 1
⊢ ResiduallyFinite (G × G')

Tactic:
rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup]

Premises used: Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
inst_3 : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
fst : g.1 = 1.1
snd : g.2 = 1.2
⊢ g = 1

Tactic:
ext
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
inst_3 : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g.1 = 1.1

Tactic:
eq_one_iff_forall_finiteIndexNormalSubroup g.1 fun K ↦ hg (K.comap (MonoidHom.fst G G'))

Premises used: Prod.fst, MonoidHom.fst, Group.eq_one_iff_forall_finiteIndexNormalSubroup, FiniteIndexNormalSubgroup.comap
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
inst_3 : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g.1 = 1.1

Tactic:
exact eq_one_iff_forall_finiteIndexNormalSubroup g.1 fun K ↦ hg (K.comap (MonoidHom.fst G G'))

Premises used: Prod.fst, MonoidHom.fst, Group.eq_one_iff_forall_finiteIndexNormalSubroup, FiniteIndexNormalSubgroup.comap
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
inst_3 : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g.2 = 1.2

Tactic:
eq_one_iff_forall_finiteIndexNormalSubroup g.2 fun K ↦ hg (K.comap (MonoidHom.snd G G'))

Premises used: Group.eq_one_iff_forall_finiteIndexNormalSubroup, FiniteIndexNormalSubgroup.comap, Prod.snd, MonoidHom.snd
-- Module: Mathlib.GroupTheory.ResiduallyFinite
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
inst_3 : ResiduallyFinite G'
g : G × G'
hg : ∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H
⊢ g.2 = 1.2

Tactic:
exact eq_one_iff_forall_finiteIndexNormalSubroup g.2 fun K ↦ hg (K.comap (MonoidHom.snd G G'))

Premises used: Group.eq_one_iff_forall_finiteIndexNormalSubroup, FiniteIndexNormalSubgroup.comap, Prod.snd, MonoidHom.snd
-- 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
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

Tactic:
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G

Premises used: Group.rank_spec
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
rw : Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

Tactic:
rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]

Premises used: Finset.card_univ, Finset.prod_const, Fintype.card_coe
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
rw : (↑S : Set G) ⊆ (↑f.range : Set G)
⊢ Function.Surjective (α := (g : ↥S) → ↥(zpowers (↑g : G))) (β := G) (⇑f : (a : (g : ↥S) → ↥(zpowers (↑g : G))) → G)

Tactic:
rw [← MonoidHom.range_eq_top, eq_top_iff, ← hS2, closure_le]

Premises used: eq_top_iff, Subgroup.closure_le, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
⊢ (↑S : Set G) ⊆ (↑f.range : Set G)

Tactic:
fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩

Premises used: Set.Mem, setOf, Subgroup.mem_zpowers, Subgroup.noncommPiCoprod_mulSingle, Set.Subset, Subtype.mk, Exists.intro, Set.range, Pi.mulSingle
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
⊢ (↑S : Set G) ⊆ (↑f.range : Set G)

Tactic:
exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
⊢ Function.Surjective (α := (g : ↥S) → ↥(zpowers (↑g : G))) (β := G) (⇑f : (a : (g : ↥S) → ↥(zpowers (↑g : G))) → G)

Tactic:
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 _ _⟩
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
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 ∣ Nat.card.{u_1} ((g : ↥S) → ↥(zpowers (↑g : G)))

Tactic:
replace hf := card_dvd_of_surjective f hf
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ Nat.card.{u_1} ((g : ↥S) → ↥(zpowers (↑g : G)))
⊢ Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))

Tactic:
rw [Nat.card_pi] at hf

Premises used: Nat.card_pi
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))
⊢ Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G

Tactic:
hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)

Premises used: Finset.prod_dvd_prod_of_dvd, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))
refine :
  ∀ (g : ↥S), Membership.mem (γ := Finset ↥S) Finset.univ g → Nat.card.{u_1} ↥(zpowers (↑g : G)) ∣ Monoid.exponent G
⊢ Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G

Tactic:
refine hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)

Premises used: Finset.prod_dvd_prod_of_dvd, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))
g : ↥S
h : Membership.mem (γ := Finset ↥S) Finset.univ g
rw : orderOf (↑g : G) ∣ Monoid.exponent G
⊢ Nat.card.{u_1} ↥(zpowers (↑g : G)) ∣ Monoid.exponent G

Tactic:
rw [Nat.card_zpowers]

Premises used: Nat.card_zpowers
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))
g : ↥S
h : Membership.mem (γ := Finset ↥S) Finset.univ g
⊢ orderOf (↑g : G) ∣ Monoid.exponent G

Tactic:
Monoid.order_dvd_exponent (g : G)

Premises used: Monoid.order_dvd_exponent, Subtype.val
-- Module: Mathlib.GroupTheory.Schreier
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : Eq (α := Subgroup G) (closure (↑S : Set G)) ⊤
f : ((g : ↥S) → ↥(zpowers (↑g : G))) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))
g : ↥S
h : Membership.mem (γ := Finset ↥S) Finset.univ g
⊢ orderOf (↑g : G) ∣ Monoid.exponent G

Tactic:
exact Monoid.order_dvd_exponent (g : G)

Premises used: Monoid.order_dvd_exponent, Subtype.val