-- Mathlib/GroupTheory/Schreier.lean
theorem card_dvd_exponent_pow_rank : Nat.card G ∣ Monoid.exponent G ^ Group.rank G

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ orderOf ↑g ∣ Monoid.exponent G

Tactic:
exact Monoid.order_dvd_exponent (g : G)

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Function.Surjective ⇑f
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Tactic:
replace hf := card_dvd_of_surjective f hf

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → ↥(zpowers ↑g))
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ Nat.card ↥(zpowers ↑g) ∣ Monoid.exponent G

Tactic:
rw [Nat.card_zpowers]

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ orderOf ↑g ∣ Monoid.exponent G

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG 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)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

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

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ ↑S ⊆ ↑f.range

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

Result:
no goals

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent 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 _ _⟩

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Function.Surjective ⇑f
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Tactic:
let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → ↥(zpowers ↑g))
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Tactic:
rw [Nat.card_pi] at hf

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

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

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card ↥(zpowers ↑a)
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ Nat.card ↥(zpowers ↑g) ∣ Monoid.exponent G

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G

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

Result:
case intro.intro
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ Function.Surjective ⇑f

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

Result:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : S.card = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
⊢ ↑S ⊆ ↑f.range