[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))) * R = ⊤
[PROOFSTEP]
let f : G → R := fun g => toFun hR g
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
⊢ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))) * R = ⊤
[PROOFSTEP]
let U : Set G := (R * S).image fun g => g * (f g : G)⁻¹
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
⊢ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))) * R = ⊤
[PROOFSTEP]
change (closure U : Set G) * R = ⊤
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
⊢ ↑(closure U) * R = ⊤
[PROOFSTEP]
refine' top_le_iff.mp fun g _ => _
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ g ∈ ↑(closure U) * R
[PROOFSTEP]
apply closure_induction_right (eq_top_iff.mp hS (mem_top g))
[GOAL]
case H1
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ 1 ∈ ↑(closure U) * R
[PROOFSTEP]
exact ⟨1, 1, (closure U).one_mem, hR1, one_mul 1⟩
[GOAL]
case Hmul
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ ∀ (x y : G), y ∈ S → x ∈ ↑(closure U) * R → x * y ∈ ↑(closure U) * R
[PROOFSTEP]
rintro - s hs ⟨u, r, hu, hr, rfl⟩
[GOAL]
case Hmul.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ (fun x x_1 => x * x_1) u r * s ∈ ↑(closure U) * R
[PROOFSTEP]
rw [show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * r * s = u * (r * s * (↑(f (r * s)))⁻¹) * ↑(f (r * s))
[PROOFSTEP]
group
[GOAL]
case Hmul.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * (r * s * (↑(f (r * s)))⁻¹) * ↑(f (r * s)) ∈ ↑(closure U) * R
[PROOFSTEP]
refine' Set.mul_mem_mul ((closure U).mul_mem hu _) (f (r * s)).coe_prop
[GOAL]
case Hmul.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ r * s * (↑(f (r * s)))⁻¹ ∈ closure U
[PROOFSTEP]
exact subset_closure ⟨r * s, Set.mul_mem_mul hr hs, rfl⟩
[GOAL]
case Hinv
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
⊢ ∀ (x y : G), y ∈ S → x ∈ ↑(closure U) * R → x * y⁻¹ ∈ ↑(closure U) * R
[PROOFSTEP]
rintro - s hs ⟨u, r, hu, hr, rfl⟩
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ (fun x x_1 => x * x_1) u r * s⁻¹ ∈ ↑(closure U) * R
[PROOFSTEP]
rw [show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹) by group]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * r * s⁻¹ = u * (↑(f (r * s⁻¹)) * s * r⁻¹)⁻¹ * ↑(f (r * s⁻¹))
[PROOFSTEP]
group
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ u * (↑(f (r * s⁻¹)) * s * r⁻¹)⁻¹ * ↑(f (r * s⁻¹)) ∈ ↑(closure U) * R
[PROOFSTEP]
refine' Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem _)) (f (r * s⁻¹)).2
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * s * r⁻¹ ∈ closure U
[PROOFSTEP]
refine' subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, _⟩
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ (fun g => g * (↑(f g))⁻¹) (↑(f (r * s⁻¹)) * s) = ↑(f (r * s⁻¹)) * s * r⁻¹
[PROOFSTEP]
rw [mul_right_inj, inv_inj, ← Subtype.coe_mk r hr, ← Subtype.ext_iff, Subtype.coe_mk]
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ f (↑(toFun hR (↑{ val := r, property := hr } * s⁻¹)) * s) = { val := r, property := hr }
[PROOFSTEP]
apply
  (mem_rightTransversals_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
    (mul_inv_toFun_mem hR (f (r * s⁻¹) * s))
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * s * (↑{ val := r, property := hr })⁻¹ ∈ ↑H
[PROOFSTEP]
rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]
[GOAL]
case Hinv.intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
f : G → ↑R := fun g => toFun hR g
U : Set G := (fun g => g * (↑(f g))⁻¹) '' (R * S)
g : G
x✝ : g ∈ ⊤
s : G
hs : s ∈ S
u r : G
hu : u ∈ ↑(closure U)
hr : r ∈ R
⊢ ↑(f (r * s⁻¹)) * (↑{ val := r, property := hr } * s⁻¹)⁻¹ ∈ ↑H
[PROOFSTEP]
exact toFun_mul_inv_mem hR (r * s⁻¹)
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
[PROOFSTEP]
have hU : closure ((R * S).image fun g => g * (toFun hR g : G)⁻¹) ≤ H :=
  by
  rw [closure_le]
  rintro - ⟨g, -, rfl⟩
  exact mul_inv_toFun_mem hR g
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
[PROOFSTEP]
rw [closure_le]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ (fun g => g * (↑(toFun hR g))⁻¹) '' (R * S) ⊆ ↑H
[PROOFSTEP]
rintro - ⟨g, -, rfl⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
g : G
⊢ (fun g => g * (↑(toFun hR g))⁻¹) g ∈ ↑H
[PROOFSTEP]
exact mul_inv_toFun_mem hR g
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
⊢ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) = H
[PROOFSTEP]
refine' le_antisymm hU fun h hh => _
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
h : G
hh : h ∈ H
⊢ h ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
[PROOFSTEP]
obtain ⟨g, r, hg, hr, rfl⟩ := show h ∈ _ from eq_top_iff.mp (closure_mul_image_mul_eq_top hR hR1 hS) (mem_top h)
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ (fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
[PROOFSTEP]
suffices (⟨r, hr⟩ : R) = (⟨1, hR1⟩ : R) by simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
this : { val := r, property := hr } = { val := 1, property := hR1 }
⊢ (fun x x_1 => x * x_1) g r ∈ closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S))
[PROOFSTEP]
simpa only [show r = 1 from Subtype.ext_iff.mp this, mul_one]
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ { val := r, property := hr } = { val := 1, property := hR1 }
[PROOFSTEP]
apply (mem_rightTransversals_iff_existsUnique_mul_inv_mem.mp hR r).unique
[GOAL]
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := r, property := hr })⁻¹ ∈ ↑H
[PROOFSTEP]
rw [Subtype.coe_mk, mul_inv_self]
[GOAL]
case intro.intro.intro.intro.py₁
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ 1 ∈ ↑H
[PROOFSTEP]
exact H.one_mem
[GOAL]
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r * (↑{ val := 1, property := hR1 })⁻¹ ∈ ↑H
[PROOFSTEP]
rw [Subtype.coe_mk, inv_one, mul_one]
[GOAL]
case intro.intro.intro.intro.py₂
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
hU : closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)) ≤ H
g r : G
hg : g ∈ ↑(closure ((fun g => g * (↑(toFun hR g))⁻¹) '' (R * S)))
hr : r ∈ R
hh : (fun x x_1 => x * x_1) g r ∈ H
⊢ r ∈ ↑H
[PROOFSTEP]
exact (H.mul_mem_cancel_left (hU hg)).mp hh
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ closure ((fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) '' (R * S)) = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← map_subtype_le_map_subtype, MonoidHom.map_closure, Set.image_image]
[GOAL]
G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ map (Subgroup.subtype H) ⊤ ≤
    closure
      ((fun x => ↑(Subgroup.subtype H) { val := x * (↑(toFun hR x))⁻¹, property := (_ : x * (↑(toFun hR x))⁻¹ ∈ H) }) ''
        (R * S))
[PROOFSTEP]
exact (map_subtype_le ⊤).trans (ge_of_eq (closure_mul_image_eq hR hR1 hS))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : DecidableEq G
R S : Finset G
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure
      ↑(Finset.image (fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) (R * S)) =
    ⊤
[PROOFSTEP]
rw [Finset.coe_image, Finset.coe_mul]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : DecidableEq G
R S : Finset G
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
hS : closure ↑S = ⊤
⊢ closure ((fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) '' (↑R * ↑S)) = ⊤
[PROOFSTEP]
exact closure_mul_image_eq_top hR hR1 hS
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
letI := H.fintypeQuotientOfFiniteIndex
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
haveI : DecidableEq G := Classical.decEq G
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
obtain ⟨R₀, hR : R₀ ∈ rightTransversals (H : Set G), hR1⟩ := exists_right_transversal (1 : G)
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
haveI : Fintype R₀ := Fintype.ofEquiv _ (toEquiv hR)
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
let R : Finset G := Set.toFinset R₀
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
replace hR : (R : Set G) ∈ rightTransversals (H : Set G) := by rwa [Set.coe_toFinset]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR : R₀ ∈ rightTransversals ↑H
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
⊢ ↑R ∈ rightTransversals ↑H
[PROOFSTEP]
rwa [Set.coe_toFinset]
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
replace hR1 : (1 : G) ∈ R := by rwa [Set.mem_toFinset]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
⊢ 1 ∈ R
[PROOFSTEP]
rwa [Set.mem_toFinset]
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ ∃ T, Finset.card T ≤ index H * Finset.card S ∧ closure ↑T = ⊤
[PROOFSTEP]
refine' ⟨_, _, closure_mul_image_eq_top' hR hR1 hS⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ Finset.card
      (Finset.image (fun g => { val := g * (↑(toFun hR g))⁻¹, property := (_ : g * (↑(toFun hR g))⁻¹ ∈ H) }) (R * S)) ≤
    index H * Finset.card S
[PROOFSTEP]
calc
  _ ≤ (R * S).card := Finset.card_image_le
  _ ≤ (R ×ˢ S).card := Finset.card_image_le
  _ = R.card * S.card := (R.card_product S)
  _ = H.index * S.card := congr_arg (· * S.card) ?_
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R✝ S✝ : Set G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
this✝ : DecidableEq G
R₀ : Set G
this : Fintype ↑R₀
R : Finset G := Set.toFinset R₀
hR : ↑R ∈ rightTransversals ↑H
hR1 : 1 ∈ R
⊢ Finset.card R = index H
[PROOFSTEP]
calc
  R.card = Fintype.card R := (Fintype.card_coe R).symm
  _ = _ := (Fintype.card_congr (toEquiv hR)).symm
  _ = Fintype.card (G ⧸ H) := (QuotientGroup.card_quotient_rightRel H)
  _ = H.index := H.index_eq_card.symm
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
⊢ Group.FG { x // x ∈ H }
[PROOFSTEP]
obtain ⟨S, hS⟩ := hG.1
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
⊢ Group.FG { x // x ∈ H }
[PROOFSTEP]
obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
S : Finset G
hS : closure ↑S = ⊤
T : Finset { x // x ∈ H }
hT : closure ↑T = ⊤
⊢ Group.FG { x // x ∈ H }
[PROOFSTEP]
exact ⟨⟨T, hT⟩⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
haveI := H.fg_of_index_ne_zero
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G
[GOAL]
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
S : Finset G
hS₀ : Finset.card S = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S✝ : Set G
hG : Group.FG G
inst✝ : FiniteIndex H
this : Group.FG { x // x ∈ H }
S : Finset G
hS₀ : Finset.card S = Group.rank G
hS : closure ↑S = ⊤
T : Finset { x // x ∈ H }
hT₀ : Finset.card T ≤ index H * Finset.card S
hT : closure ↑T = ⊤
⊢ Group.rank { x // x ∈ H } ≤ index H * Group.rank G
[PROOFSTEP]
calc
  Group.rank H ≤ T.card := Group.rank_le H hT
  _ ≤ H.index * S.card := hT₀
  _ = H.index * Group.rank G := congr_arg ((· * ·) H.index) hS₀
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
by_cases hG : (center G).index = 0
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
simp_rw [hG, zero_mul, zero_add, pow_one, dvd_zero]
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
haveI : FiniteIndex (center G) :=
  ⟨hG⟩
    -- Rewrite as `|Z(G) ∩ G'| * [G' : Z(G) ∩ G'] ∣ [G : Z(G)] ^ ([G : Z(G)] * n) * [G : Z(G)]`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ∣ index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G) + 1)
[PROOFSTEP]
rw [← ((center G).subgroupOf (_root_.commutator G)).card_mul_index, pow_succ']
  -- We have `h1 : [G' : Z(G) ∩ G'] ∣ [G : Z(G)]`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
[PROOFSTEP]
have h1 :=
  relindex_dvd_index_of_normal (center G)
    (_root_.commutator G)
      -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ ([G : Z(G)] * n)`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } *
      index (subgroupOf (center G) (_root_.commutator G)) ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G)) * index (center G)
[PROOFSTEP]
refine' mul_dvd_mul _ h1
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
haveI : FiniteIndex ((center G).subgroupOf (_root_.commutator G)) :=
  ⟨ne_zero_of_dvd_ne_zero hG h1⟩
    -- We have `h2 : rank (Z(G) ∩ G') ≤ [G' : Z(G) ∩ G'] * rank G'` by Schreier's lemma
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h2 :=
  rank_le_index_mul_rank
    ((center G).subgroupOf (_root_.commutator G))
      -- We have `h3 : [G' : Z(G) ∩ G'] * rank G' ≤ [G : Z(G)] * n` by `h1` and `rank G' ≤ n`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h3 :=
  Nat.mul_le_mul (Nat.le_of_dvd (Nat.pos_of_ne_zero hG) h1)
    (rank_commutator_le_card G)
      -- So we can reduce to proving `|Z(G) ∩ G'| ∣ [G : Z(G)] ^ rank (Z(G) ∩ G')`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ (index (center G) * Nat.card ↑(commutatorSet G))
[PROOFSTEP]
refine'
  dvd_trans _
    (pow_dvd_pow (center G).index (h2.trans h3))
      -- `Z(G) ∩ G'` is abelian, so it enough to prove that `g ^ [G : Z(G)] = 1` for `g ∈ Z(G) ∩ G'`
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ∣
    index (center G) ^ Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
[PROOFSTEP]
apply card_dvd_exponent_pow_rank'
[GOAL]
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
⊢ ∀ (g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }), g ^ index (center G) = 1
[PROOFSTEP]
intro g
[GOAL]
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
⊢ g ^ index (center G) = 1
[PROOFSTEP]
have :=
  Abelianization.commutator_subset_ker (MonoidHom.transferCenterPow G)
    g.1.2
      -- `transfer g` is defeq to `g ^ [G : Z(G)]`, so we are done
[GOAL]
case neg.hG
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬index (center G) = 0
this✝¹ : FiniteIndex (center G)
h1 : relindex (center G) (_root_.commutator G) ∣ index (center G)
this✝ : FiniteIndex (subgroupOf (center G) (_root_.commutator G))
h2 :
  Group.rank { x // x ∈ subgroupOf (center G) (_root_.commutator G) } ≤
    index (subgroupOf (center G) (_root_.commutator G)) * Group.rank { x // x ∈ _root_.commutator G }
h3 :
  relindex (center G) (_root_.commutator G) * Group.rank { x // x ∈ _root_.commutator G } ≤
    index (center G) * Nat.card ↑(commutatorSet G)
g : { x // x ∈ subgroupOf (center G) (_root_.commutator G) }
this : ↑↑g ∈ MonoidHom.ker (MonoidHom.transferCenterPow G)
⊢ g ^ index (center G) = 1
[PROOFSTEP]
simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using this
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h1 := index_center_le_pow (closureCommutatorRepresentatives G)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) ^
      Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
rw [card_commutatorSet_closureCommutatorRepresentatives] at h1 h2 
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
rw [card_commutator_closureCommutatorRepresentatives] at h2 
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ Group.rank { x // x ∈ closureCommutatorRepresentatives G }
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
replace h1 := h1.trans (Nat.pow_le_pow_of_le_right Finite.card_pos (rank_closureCommutatorRepresentatives_le G))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) * Nat.card ↑(commutatorSet G) + 1)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
replace h2 := h2.trans (pow_dvd_pow _ (add_le_add_right (mul_le_mul_right' h1 _) 1))
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G)) * Nat.card ↑(commutatorSet G) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
rw [← pow_succ'] at h2 
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ Nat.card { x // x ∈ _root_.commutator G } ≤ cardCommutatorBound (Nat.card ↑(commutatorSet G))
[PROOFSTEP]
refine' (Nat.le_of_dvd _ h2).trans (Nat.pow_le_pow_of_le_left h1 _)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h1 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ≤
    Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G))
h2 :
  Nat.card { x // x ∈ _root_.commutator G } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
⊢ 0 <
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (Nat.card ↑(commutatorSet G) ^ (2 * Nat.card ↑(commutatorSet G) + 1) + 1)
[PROOFSTEP]
exact pow_pos (Nat.pos_of_ne_zero FiniteIndex.finiteIndex) _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
⊢ Finite { x // x ∈ _root_.commutator G }
[PROOFSTEP]
have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
⊢ Finite { x // x ∈ _root_.commutator G }
[PROOFSTEP]
refine' Nat.finite_of_card_ne_zero fun h => _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  Nat.card { x // x ∈ _root_.commutator { x // x ∈ closureCommutatorRepresentatives G } } ∣
    index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1)
h : Nat.card { x // x ∈ _root_.commutator G } = 0
⊢ False
[PROOFSTEP]
rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2 
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
R S : Set G
inst✝ : Finite ↑(commutatorSet G)
h2 :
  index (center { x // x ∈ closureCommutatorRepresentatives G }) ^
      (index (center { x // x ∈ closureCommutatorRepresentatives G }) *
          Nat.card ↑(commutatorSet { x // x ∈ closureCommutatorRepresentatives G }) +
        1) =
    0
h : Nat.card { x // x ∈ _root_.commutator G } = 0
⊢ False
[PROOFSTEP]
exact FiniteIndex.finiteIndex (pow_eq_zero h2)
