awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 : ℕ)
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
have 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 : ℕ)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 : ℕ)
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₂ : HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) =
  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]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 : ℕ)
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₃ : HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) =
  HPow.hPow (β := ℕ) p (((Nat.card α).factorial.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]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 : ℕ)
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₄ : HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) =
  HPow.hPow (β := ℕ) p (((p ^ n).factorial.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]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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 : ℕ)
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₅ : HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) = p ^ multiplicity p (p ^ n).factorial
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]
-- Lean 4 proof step from Mathlib.GroupTheory.RegularWreathProduct (goal)
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
⊢ Nat.card.{u_3} ↥f.range = HPow.hPow (β := ℕ) p (((Nat.card.{u_3} (Equiv.Perm α)).factorization : (a : ℕ) → ℕ) p : ℕ)
have rw₆ : HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i) = HPow.hPow (β := ℕ) p (∑ i ∈ Finset.range n, p ^ i)
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]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
Goal:
G : Type u_1
inst : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
have simp_rw : Eq.{u_1 + 1} (α := Subgroup G) (⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup) ⊥ ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
have 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
Tactic: simp_rw [residuallyFinite_def, Subgroup.eq_bot_iff_forall, Subgroup.mem_iInf,
    FiniteIndexNormalSubgroup.mem_toSubgroup_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
have simp_rw₂ : (∀ (x : G), (∀ (i : FiniteIndexNormalSubgroup G), x ∈ i.toSubgroup) → x = 1) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
Goal:
G : Type u_1
inst : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H
have simp_rw : (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
  ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H
Tactic: simp_rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup, ← not_forall, not_imp_not]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H
have simp_rw₁ : (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
  ∀ (g : G), g ≠ 1 → ¬∀ (x : FiniteIndexNormalSubgroup G), g ∈ x
Tactic: simp_rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup, ← not_forall, not_imp_not]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
Goal:
G : Type u_1
inst : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1
have rw : (∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1) ↔
  ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1
Tactic: rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
Goal:
G : Type u_1
inst : Group G
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
have simp_rw : (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
have simp_rw₁ : (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔
  ∀ (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]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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)
⊢ ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
have simp_rw₂ : (∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1) ↔
  ∀ (g : G), g ≠ 1 → ¬∀ (x : Subgroup G), x.FiniteIndex → g ∈ x
Tactic: simp_rw [residuallyFinite_iff_forall_finiteIndex, ← Classical.not_imp, ← not_forall,
    not_imp_not]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : ResiduallyFinite G
g h : G
hgh : g ≠ h
⊢ ∃ (H : FiniteIndexNormalSubgroup G), Ne (α := G ⧸ H.toSubgroup) (↑g : G ⧸ H.toSubgroup) (↑h : G ⧸ H.toSubgroup)
have obtain : ∀ (H : FiniteIndexNormalSubgroup G) (hH : g⁻¹ * h ∉ H),
  ∃ (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
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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)
⊢ ResiduallyFinite G
have rw : ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
Tactic: rw [residuallyFinite_iff_exists_finiteIndex]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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
⊢ ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H
have 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
Tactic: obtain ⟨_, _, _, f, hf⟩ := h g hg
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
H : Subgroup G
⊢ ResiduallyFinite.{u_1} ↥H
have rw : ∀ (g : ↥H), (∀ (H_1 : FiniteIndexNormalSubgroup ↥H), g ∈ H_1) → g = 1
Tactic: rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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 = 1
have a : (↑g : G) = (↑1 : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
inst_2 : ResiduallyFinite G
inst_3 : ResiduallyFinite G'
⊢ ResiduallyFinite (G × G')
have rw : ∀ (g : G × G'), (∀ (H : FiniteIndexNormalSubgroup (G × G')), g ∈ H) → g = 1
Tactic: rw [residuallyFinite_iff_forall_finiteIndexNormalSubgroup]
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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
have fst : g.1 = 1.1
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.ResiduallyFinite (goal)
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
⊢ g = 1
have snd : g.2 = 1.2
Tactic: ext
-- 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: obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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)) ⊤
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
have rw : Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
Tactic: rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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)
have rw : (↑S : Set G) ⊆ (↑f.range : Set G)
Tactic: rw [← MonoidHom.range_eq_top, eq_top_iff, ← hS2, closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
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 ⋯
⊢ Nat.card G ∣ ∏ _x : ↥S, Monoid.exponent G
have hf : 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 _ _⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
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 ∣ ∏ _x : ↥S, Monoid.exponent G
have hf₁ : Nat.card G ∣ Nat.card.{u_1} ((g : ↥S) → ↥(zpowers (↑g : G)))
Tactic: replace hf := card_dvd_of_surjective f hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (hypothesis)
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 ∣ ∏ _x : ↥S, Monoid.exponent G
have hf₁ : Nat.card G ∣ ∏ a : ↥S, Nat.card.{u_1} ↥(zpowers (↑a : G))
Tactic: rw [Nat.card_pi] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
have refine : ∀ (g : ↥S), Membership.mem (γ := Finset ↥S) Finset.univ g → Nat.card.{u_1} ↥(zpowers (↑g : G)) ∣ Monoid.exponent G
Tactic: refine hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Schreier (goal)
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
⊢ Nat.card.{u_1} ↥(zpowers (↑g : G)) ∣ Monoid.exponent G
have rw : orderOf (↑g : G) ∣ Monoid.exponent G
Tactic: rw [Nat.card_zpowers]