case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ Monoid.exponent G ^ Group.rank G
rw [← hS1, ← Fintype.card_coe, ← Finset.card_univ, ← Finset.prod_const]
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
let f : (∀ g : S, zpowers (g : G)) →* G := noncommPiCoprod fun s t _ x y _ _ => mul_comm x _
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Function.Surjective ↑f
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
have hf : Function.Surjective f := by
  rw [← MonoidHom.range_top_iff_surjective, eq_top_iff, ← hS2, closure_le]
  exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Function.Surjective ↑f
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
replace hf := nat_card_dvd_of_surjective f hf
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
rw [Nat.card_pi] at hf
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ Nat.card { x // x ∈ zpowers ↑g } ∣ Monoid.exponent G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
⊢ Nat.card G ∣ ∏ _x : { x // x ∈ S }, Monoid.exponent G
refine' hf.trans (Finset.prod_dvd_prod_of_dvd _ _ fun g _ => _)
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ orderOf ↑g ∣ Monoid.exponent G
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ Nat.card { x // x ∈ zpowers ↑g } ∣ Monoid.exponent G
rw [← order_eq_card_zpowers']
no goals
case intro.intro
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
hf✝ : Nat.card G ∣ Nat.card ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g })
hf : Nat.card G ∣ ∏ a : { x // x ∈ S }, Nat.card { x // x ∈ zpowers ↑a }
g : { x // x ∈ S }
x✝ : g ∈ Finset.univ
⊢ orderOf ↑g ∣ Monoid.exponent G
exact Monoid.order_dvd_exponent (g : G)
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ ↑S ⊆ ↑(MonoidHom.range f)
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ Function.Surjective ↑f
rw [← MonoidHom.range_top_iff_surjective, eq_top_iff, ← hS2, closure_le]
no goals
G : Type u
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : Finset.card S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : { x // x ∈ S }) → { x // x ∈ zpowers ↑g }) →* G :=
  noncommPiCoprod (_ : ∀ (s t : { x // x ∈ S }), s ≠ t → ∀ (x y : G), x ∈ zpowers ↑s → y ∈ zpowers ↑t → x * y = y * x)
⊢ ↑S ⊆ ↑(MonoidHom.range f)
exact fun g hg => ⟨Pi.mulSingle ⟨g, hg⟩ ⟨g, mem_zpowers g⟩, noncommPiCoprod_mulSingle _ _⟩