[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
a b : G
ha : a ∈ {x | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H}
hb : b ∈ {x | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H}
y : G
⊢ a * b * y * (a * b)⁻¹ * y⁻¹ ∈ H
[PROOFSTEP]
convert Subgroup.mul_mem _ (ha (b * y * b⁻¹)) (hb y) using 1
[GOAL]
case h.e'_4
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
a b : G
ha : a ∈ {x | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H}
hb : b ∈ {x | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H}
y : G
⊢ a * b * y * (a * b)⁻¹ * y⁻¹ = a * (b * y * b⁻¹) * a⁻¹ * (b * y * b⁻¹)⁻¹ * (b * y * b⁻¹ * y⁻¹)
[PROOFSTEP]
group
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
y : G
⊢ 1 * y * 1⁻¹ * y⁻¹ ∈ H
[PROOFSTEP]
simp [Subgroup.one_mem]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x : G
hx :
  x ∈
    {
          toSubsemigroup :=
            { carrier := {x | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H},
              mul_mem' :=
                (_ :
                  ∀ {a b : G} {ha : a ∈ {x | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H}}
                    {hb : b ∈ {x | ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H}} {y : G}, a * b * y * (a * b)⁻¹ * y⁻¹ ∈ H) },
          one_mem' := (_ : ∀ (y : G), 1 * y * 1⁻¹ * y⁻¹ ∈ H) }.toSubsemigroup.carrier
y : G
⊢ x⁻¹ * y * x⁻¹⁻¹ * y⁻¹ ∈ H
[PROOFSTEP]
specialize hx y⁻¹
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x y : G
hx : x * y⁻¹ * x⁻¹ * y⁻¹⁻¹ ∈ H
⊢ x⁻¹ * y * x⁻¹⁻¹ * y⁻¹ ∈ H
[PROOFSTEP]
rw [mul_assoc, inv_inv] at hx ⊢
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x y : G
hx : x * y⁻¹ * (x⁻¹ * y) ∈ H
⊢ x⁻¹ * y * (x * y⁻¹) ∈ H
[PROOFSTEP]
exact Subgroup.Normal.mem_comm inferInstance hx
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ upperCentralSeriesStep H = comap (mk' H) (center (G ⧸ H))
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ x✝ ∈ comap (mk' H) (center (G ⧸ H))
[PROOFSTEP]
rw [mem_comap, mem_center_iff, forall_mk]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ ∀ (x : G), ↑x * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑x
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ ∀ (a : G), x✝ * a * x✝⁻¹ * a⁻¹ ∈ H ↔ ↑a * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑a
[PROOFSTEP]
intro y
[GOAL]
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ ∈ H ↔ ↑y * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑y
[PROOFSTEP]
rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem, div_eq_mul_inv, mul_inv_rev,
  mul_assoc]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Normal (upperCentralSeriesStep H)
[PROOFSTEP]
rw [upperCentralSeriesStep_eq_comap_center]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Normal (comap (mk' H) (center (G ⧸ H)))
[PROOFSTEP]
infer_instance
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ upperCentralSeries G 1 = center G
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G
[PROOFSTEP]
simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep, center, Set.center, mem_mk, mem_bot,
  Set.mem_setOf_eq]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ (∀ (y : G), x✝ * y * x✝⁻¹ * y⁻¹ = 1) ↔ ∀ (m : G), m * x✝ = x✝ * m
[PROOFSTEP]
exact forall_congr' fun y => by rw [mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ = 1 ↔ y * x✝ = x✝ * y
[PROOFSTEP]
rw [mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
⊢ H (n + 1) ≤ upperCentralSeries G (n + 1)
[PROOFSTEP]
intro x hx
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ x ∈ upperCentralSeries G (n + 1)
[PROOFSTEP]
rw [mem_upperCentralSeries_succ_iff]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n
[PROOFSTEP]
exact fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Monotone (upperCentralSeries G)
[PROOFSTEP]
refine' monotone_nat_of_le_succ _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (n : ℕ), upperCentralSeries G n ≤ upperCentralSeries G (n + 1)
[PROOFSTEP]
intro n x hx y
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G (Nat.add n 0)).fst
[PROOFSTEP]
rw [mul_assoc, mul_assoc, ← mul_assoc y x⁻¹ y⁻¹]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * (y * x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G (Nat.add n 0)).fst
[PROOFSTEP]
exact mul_mem hx (Normal.conj_mem (upperCentralSeries_normal G n) x⁻¹ (inv_mem hx) y)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Group.IsNilpotent G ↔ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Group.IsNilpotent G → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
rintro ⟨n, nH⟩
[GOAL]
case mp.mk.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
nH : upperCentralSeries G n = ⊤
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
refine' ⟨_, _, upperCentralSeries_isAscendingCentralSeries G, nH⟩
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → Group.IsNilpotent G
[PROOFSTEP]
rintro ⟨n, H, hH, hn⟩
[GOAL]
case mpr.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ Group.IsNilpotent G
[PROOFSTEP]
use n
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤
[PROOFSTEP]
rw [eq_top_iff, ← hn]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n
[PROOFSTEP]
exact ascending_central_series_le_upper H hH n
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
hasc : IsAscendingCentralSeries H
⊢ IsDescendingCentralSeries fun m => H (n - m)
[PROOFSTEP]
cases' hasc with h0 hH
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
⊢ IsDescendingCentralSeries fun m => H (n - m)
[PROOFSTEP]
refine' ⟨hn, fun x m hx g => _⟩
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x ∈ (fun m => H (n - m)) m
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
dsimp at hx
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
by_cases hm : n ≤ m
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : n ≤ m
⊢ x * g * x⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x = 1
g : G
hm : n ≤ m
⊢ x * g * x⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
subst hx
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ 1 * g * 1⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
rw [show (1 : G) * g * (1⁻¹ : G) * g⁻¹ = 1 by group]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ 1 * g * 1⁻¹ * g⁻¹ = 1
[PROOFSTEP]
group
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ 1 ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
exact Subgroup.one_mem _
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : ¬n ≤ m
⊢ x * g * x⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
push_neg at hm
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ x * g * x⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) (m + 1)
[PROOFSTEP]
apply hH
[GOAL]
case neg.a
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ x ∈ H (n - (m + 1) + 1)
[PROOFSTEP]
convert hx using 1
[GOAL]
case h.e'_5
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : m < n
⊢ H (n - (m + 1) + 1) = H (n - m)
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_sub_succ]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
⊢ IsAscendingCentralSeries fun m => H (n - m)
[PROOFSTEP]
cases' hdesc with h0 hH
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ IsAscendingCentralSeries fun m => H (n - m)
[PROOFSTEP]
refine' ⟨hn, fun x m hx g => _⟩
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ (fun m => H (n - m)) (m + 1)
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ (fun m => H (n - m)) m
[PROOFSTEP]
dsimp only at hx ⊢
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ H (n - m)
[PROOFSTEP]
by_cases hm : n ≤ m
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
⊢ x * g * x⁻¹ * g⁻¹ ∈ H (n - m)
[PROOFSTEP]
have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
hnm : n - m = 0
⊢ x * g * x⁻¹ * g⁻¹ ∈ H (n - m)
[PROOFSTEP]
rw [hnm, h0]
[GOAL]
case pos
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
hnm : n - m = 0
⊢ x * g * x⁻¹ * g⁻¹ ∈ ⊤
[PROOFSTEP]
exact mem_top _
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : ¬n ≤ m
⊢ x * g * x⁻¹ * g⁻¹ ∈ H (n - m)
[PROOFSTEP]
push_neg at hm
[GOAL]
case neg
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : m < n
⊢ x * g * x⁻¹ * g⁻¹ ∈ H (n - m)
[PROOFSTEP]
convert hH x _ hx g using 1
[GOAL]
case h.e'_5
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : m < n
⊢ H (n - m) = H (n - (m + 1) + 1)
[PROOFSTEP]
rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_sub_succ]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Group.IsNilpotent G ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
rw [nilpotent_iff_finite_ascending_central_series]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
rintro ⟨n, H, hH, hn⟩
[GOAL]
case mp.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
refine ⟨n, fun m => H (n - m), is_decending_rev_series_of_is_ascending G hn hH, ?_⟩
[GOAL]
case mp.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ (fun m => H (n - m)) n = ⊥
[PROOFSTEP]
dsimp only
[GOAL]
case mp.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥
[PROOFSTEP]
rw [tsub_self]
[GOAL]
case mp.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥
[PROOFSTEP]
exact hH.1
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
rintro ⟨n, H, hH, hn⟩
[GOAL]
case mpr.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
refine ⟨n, fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
[GOAL]
case mpr.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ (fun m => H (n - m)) n = ⊤
[PROOFSTEP]
dsimp only
[GOAL]
case mpr.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤
[PROOFSTEP]
rw [tsub_self]
[GOAL]
case mpr.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤
[PROOFSTEP]
exact hH.1
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
⊢ Normal (lowerCentralSeries G n)
[PROOFSTEP]
induction' n with d hd
[GOAL]
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Normal (lowerCentralSeries G Nat.zero)
[PROOFSTEP]
exact (⊤ : Subgroup G).normal_of_characteristic
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
d : ℕ
hd : Normal (lowerCentralSeries G d)
⊢ Normal (lowerCentralSeries G (Nat.succ d))
[PROOFSTEP]
exact @Subgroup.commutator_normal _ _ (lowerCentralSeries G d) ⊤ hd _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Antitone (lowerCentralSeries G)
[PROOFSTEP]
refine' antitone_nat_of_succ_le fun n x hx => _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ lowerCentralSeries G (n + 1)
⊢ x ∈ lowerCentralSeries G n
[PROOFSTEP]
simp only [mem_lowerCentralSeries_succ_iff, exists_prop, mem_top, exists_true_left, true_and_iff] at hx
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ x ∈ lowerCentralSeries G n
[PROOFSTEP]
refine' closure_induction hx _ (Subgroup.one_mem _) (@Subgroup.mul_mem _ _ _) (@Subgroup.inv_mem _ _ _)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ ∀ (x : G), x ∈ {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x} → x ∈ lowerCentralSeries G n
[PROOFSTEP]
rintro y ⟨z, hz, a, ha⟩
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ y ∈ lowerCentralSeries G n
[PROOFSTEP]
rw [← ha, mul_assoc, mul_assoc, ← mul_assoc a z⁻¹ a⁻¹]
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ z * (a * z⁻¹ * a⁻¹) ∈ lowerCentralSeries G n
[PROOFSTEP]
exact mul_mem hz (Normal.conj_mem (lowerCentralSeries_normal n) z⁻¹ (inv_mem hz) a)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ IsDescendingCentralSeries (lowerCentralSeries G)
[PROOFSTEP]
constructor
[GOAL]
case left
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ lowerCentralSeries G 0 = ⊤
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
[PROOFSTEP]
rfl
[GOAL]
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
[PROOFSTEP]
intro x n hxn g
[GOAL]
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x : G
n : ℕ
hxn : x ∈ lowerCentralSeries G n
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
[PROOFSTEP]
exact commutator_mem_commutator hxn (mem_top g)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Group.IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥
[PROOFSTEP]
rw [nilpotent_iff_finite_descending_central_series]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) ↔ ∃ n, lowerCentralSeries G n = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n, lowerCentralSeries G n = ⊥
[PROOFSTEP]
rintro ⟨n, H, ⟨h0, hs⟩, hn⟩
[GOAL]
case mp.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ ∃ n, lowerCentralSeries G n = ⊥
[PROOFSTEP]
use n
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← hn]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
n : ℕ
H : ℕ → Subgroup G
hn : H n = ⊥
h0 : H 0 = ⊤
hs : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H (n + 1)
⊢ lowerCentralSeries G n ≤ H n
[PROOFSTEP]
exact descending_central_series_ge_lower H ⟨h0, hs⟩ n
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ (∃ n, lowerCentralSeries G n = ⊥) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
rintro ⟨n, hn⟩
[GOAL]
case mpr.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
exact ⟨n, lowerCentralSeries G, lowerCentralSeries_isDescendingCentralSeries, hn⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ ↔ nilpotencyClass G ≤ n
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries G n = ⊤ → nilpotencyClass G ≤ n
[PROOFSTEP]
intro h
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ nilpotencyClass G ≤ n
[PROOFSTEP]
exact Nat.find_le h
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → upperCentralSeries G n = ⊤
[PROOFSTEP]
intro h
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G n = ⊤
[PROOFSTEP]
apply eq_top_iff.mpr
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ ⊤ ≤ upperCentralSeries G n
[PROOFSTEP]
rw [← upperCentralSeries_nilpotencyClass]
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n
[PROOFSTEP]
exact upperCentralSeries_mono _ h
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) = nilpotencyClass G
[PROOFSTEP]
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
[GOAL]
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
intro n hn
[GOAL]
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩
[GOAL]
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → upperCentralSeries G n = ⊤
[PROOFSTEP]
rintro n ⟨H, ⟨hH, hn⟩⟩
[GOAL]
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤
[PROOFSTEP]
rw [← top_le_iff, ← hn]
[GOAL]
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n
[PROOFSTEP]
exact ascending_central_series_le_upper H hH n
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) = nilpotencyClass G
[PROOFSTEP]
rw [← least_ascending_central_series_length_eq_nilpotencyClass]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) =
    Nat.find (_ : ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤)
[PROOFSTEP]
refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
[GOAL]
case refine_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
rintro n ⟨H, ⟨hH, hn⟩⟩
[GOAL]
case refine_1.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
refine ⟨fun m => H (n - m), is_decending_rev_series_of_is_ascending G hn hH, ?_⟩
[GOAL]
case refine_1.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ (fun m => H (n - m)) n = ⊥
[PROOFSTEP]
dsimp only
[GOAL]
case refine_1.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H (n - n) = ⊥
[PROOFSTEP]
rw [tsub_self]
[GOAL]
case refine_1.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H 0 = ⊥
[PROOFSTEP]
exact hH.1
[GOAL]
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
rintro n ⟨H, ⟨hH, hn⟩⟩
[GOAL]
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ H, IsAscendingCentralSeries H ∧ H n = ⊤
[PROOFSTEP]
refine ⟨fun m => H (n - m), is_ascending_rev_series_of_is_descending G hn hH, ?_⟩
[GOAL]
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ (fun m => H (n - m)) n = ⊤
[PROOFSTEP]
dsimp only
[GOAL]
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H (n - n) = ⊤
[PROOFSTEP]
rw [tsub_self]
[GOAL]
case refine_2.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ H 0 = ⊤
[PROOFSTEP]
exact hH.1
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) = nilpotencyClass G
[PROOFSTEP]
rw [← least_descending_central_series_length_eq_nilpotencyClass]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) = Nat.find (_ : ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥)
[PROOFSTEP]
refine' le_antisymm (Nat.find_mono _) (Nat.find_mono _)
[GOAL]
case refine'_1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), (∃ H, IsDescendingCentralSeries H ∧ H n = ⊥) → lowerCentralSeries G n = ⊥
[PROOFSTEP]
rintro n ⟨H, ⟨hH, hn⟩⟩
[GOAL]
case refine'_1.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n = ⊥
[PROOFSTEP]
rw [← le_bot_iff, ← hn]
[GOAL]
case refine'_1.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
hG : Group.IsNilpotent G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ lowerCentralSeries G n ≤ H n
[PROOFSTEP]
exact descending_central_series_ge_lower H hH n
[GOAL]
case refine'_2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
rintro n h
[GOAL]
case refine'_2
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥
[PROOFSTEP]
exact ⟨lowerCentralSeries G, ⟨lowerCentralSeries_isDescendingCentralSeries, h⟩⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass G) = ⊥
[PROOFSTEP]
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ lowerCentralSeries G (Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)) = ⊥
[PROOFSTEP]
exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ ↔ nilpotencyClass G ≤ n
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ → nilpotencyClass G ≤ n
[PROOFSTEP]
intro h
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ nilpotencyClass G ≤ n
[PROOFSTEP]
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
[GOAL]
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) ≤ n
[PROOFSTEP]
exact Nat.find_le h
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → lowerCentralSeries G n = ⊥
[PROOFSTEP]
intro h
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n = ⊥
[PROOFSTEP]
apply eq_bot_iff.mpr
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ ⊥
[PROOFSTEP]
rw [← lowerCentralSeries_nilpotencyClass]
[GOAL]
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ lowerCentralSeries G (nilpotencyClass G)
[PROOFSTEP]
exact lowerCentralSeries_antitone h
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
n : ℕ
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } n) ≤ lowerCentralSeries G n
[PROOFSTEP]
induction' n with d hd
[GOAL]
case zero
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } Nat.zero) ≤ lowerCentralSeries G Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } (Nat.succ d)) ≤ lowerCentralSeries G (Nat.succ d)
[PROOFSTEP]
rw [lowerCentralSeries_succ, lowerCentralSeries_succ, MonoidHom.map_closure]
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ closure
      (↑(Subgroup.subtype H) ''
        {x | ∃ p, p ∈ lowerCentralSeries { x // x ∈ H } d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}) ≤
    closure {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
[PROOFSTEP]
apply Subgroup.closure_mono
[GOAL]
case succ.h'
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
⊢ ↑(Subgroup.subtype H) '' {x | ∃ p, p ∈ lowerCentralSeries { x // x ∈ H } d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x} ⊆
    {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
[PROOFSTEP]
rintro x1 ⟨x2, ⟨x3, hx3, x4, _hx4, rfl⟩, rfl⟩
[GOAL]
case succ.h'.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
x3 : { x // x ∈ H }
hx3 : x3 ∈ lowerCentralSeries { x // x ∈ H } d
x4 : { x // x ∈ H }
_hx4 : x4 ∈ ⊤
⊢ ↑(Subgroup.subtype H) (x3 * x4 * x3⁻¹ * x4⁻¹) ∈
    {x | ∃ p, p ∈ lowerCentralSeries G d ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x}
[PROOFSTEP]
exact ⟨x3, hd (mem_map.mpr ⟨x3, hx3, rfl⟩), x4, by simp⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
d : ℕ
hd : Subgroup.map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } d) ≤ lowerCentralSeries G d
x3 : { x // x ∈ H }
hx3 : x3 ∈ lowerCentralSeries { x // x ∈ H } d
x4 : { x // x ∈ H }
_hx4 : x4 ∈ ⊤
⊢ ↑x4 ∈ ⊤ ∧ ↑x3 * ↑x4 * (↑x3)⁻¹ * (↑x4)⁻¹ = ↑(Subgroup.subtype H) (x3 * x4 * x3⁻¹ * x4⁻¹)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Group.IsNilpotent { x // x ∈ H }
[PROOFSTEP]
rw [nilpotent_iff_lowerCentralSeries] at *
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : ∃ n, lowerCentralSeries G n = ⊥
⊢ ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
rcases hG with ⟨n, hG⟩
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
n : ℕ
hG : lowerCentralSeries G n = ⊥
⊢ ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
use n
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
n : ℕ
hG : lowerCentralSeries G n = ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
have := lowerCentralSeries_map_subtype_le H n
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } n) ≤ lowerCentralSeries G n
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
simp only [hG, SetLike.le_def, mem_map, forall_apply_eq_imp_iff₂, exists_imp] at this
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this :
  ∀ ⦃x : G⦄ (x_1 : { x // x ∈ H }), x_1 ∈ lowerCentralSeries { x // x ∈ H } n ∧ ↑(Subgroup.subtype H) x_1 = x → x ∈ ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
exact eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ nilpotencyClass { x // x ∈ H } ≤ nilpotencyClass G
[PROOFSTEP]
repeat
  rw [← lowerCentralSeries_length_eq_nilpotencyClass]
    --- Porting note : Lean needs to be told that predicates are decidable
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ nilpotencyClass { x // x ∈ H } ≤ nilpotencyClass G
[PROOFSTEP]
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  --- Porting note : Lean needs to be told that predicates are decidable
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥) ≤ nilpotencyClass G
[PROOFSTEP]
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  --- Porting note : Lean needs to be told that predicates are decidable
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥) ≤ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)
[PROOFSTEP]
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  --- Porting note : Lean needs to be told that predicates are decidable
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries { x // x ∈ H } n = ⊥) ≤ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)
[PROOFSTEP]
refine @Nat.find_mono _ _ (Classical.decPred _) (Classical.decPred _) ?_ _ _
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
intro n hG
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
have := lowerCentralSeries_map_subtype_le H n
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : map (Subgroup.subtype H) (lowerCentralSeries { x // x ∈ H } n) ≤ lowerCentralSeries G n
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
simp only [hG, SetLike.le_def, mem_map, forall_apply_eq_imp_iff₂, exists_imp] at this
[GOAL]
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : Subgroup G
hG✝ : Group.IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this :
  ∀ ⦃x : G⦄ (x_1 : { x // x ∈ H }), x_1 ∈ lowerCentralSeries { x // x ∈ H } n ∧ ↑(Subgroup.subtype H) x_1 = x → x ∈ ⊥
⊢ lowerCentralSeries { x // x ∈ H } n = ⊥
[PROOFSTEP]
exact eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
n : ℕ
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n
[PROOFSTEP]
induction' n with d hd
[GOAL]
case zero
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
⊢ Subgroup.map f (upperCentralSeries G Nat.zero) ≤ upperCentralSeries H Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
⊢ Subgroup.map f (upperCentralSeries G (Nat.succ d)) ≤ upperCentralSeries H (Nat.succ d)
[PROOFSTEP]
rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'
[GOAL]
case succ.intro.intro
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
x : G
hx : x ∈ upperCentralSeries G (Nat.succ d)
y' : H
⊢ ↑f x * y' * (↑f x)⁻¹ * y'⁻¹ ∈ (upperCentralSeriesAux H d).fst
[PROOFSTEP]
rcases h y' with ⟨y, rfl⟩
[GOAL]
case succ.intro.intro.intro
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
d : ℕ
hd : Subgroup.map f (upperCentralSeries G d) ≤ upperCentralSeries H d
x : G
hx : x ∈ upperCentralSeries G (Nat.succ d)
y : G
⊢ ↑f x * ↑f y * (↑f x)⁻¹ * (↑f y)⁻¹ ∈ (upperCentralSeriesAux H d).fst
[PROOFSTEP]
simpa using hd (mem_map_of_mem f (hx y))
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
n : ℕ
⊢ Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n
[PROOFSTEP]
induction' n with d hd
[GOAL]
case zero
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ Subgroup.map f (lowerCentralSeries G Nat.zero) ≤ lowerCentralSeries H Nat.zero
[PROOFSTEP]
simp [Nat.zero_eq]
[GOAL]
case succ
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
⊢ Subgroup.map f (lowerCentralSeries G (Nat.succ d)) ≤ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
rintro a ⟨x, hx : x ∈ lowerCentralSeries G d.succ, rfl⟩
[GOAL]
case succ.intro.intro
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
⊢ ↑f x ∈ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
refine
  closure_induction hx ?_ (by simp [f.map_one, Subgroup.one_mem _])
    (fun y z hy hz => by simp [MonoidHom.map_mul, Subgroup.mul_mem _ hy hz])
    (fun y hy => by rw [f.map_inv]; exact Subgroup.inv_mem _ hy)
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
⊢ ↑f 1 ∈ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
simp [f.map_one, Subgroup.one_mem _]
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
y z : G
hy : ↑f y ∈ lowerCentralSeries H (Nat.succ d)
hz : ↑f z ∈ lowerCentralSeries H (Nat.succ d)
⊢ ↑f (y * z) ∈ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
simp [MonoidHom.map_mul, Subgroup.mul_mem _ hy hz]
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
y : G
hy : ↑f y ∈ lowerCentralSeries H (Nat.succ d)
⊢ ↑f y⁻¹ ∈ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
rw [f.map_inv]
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
y : G
hy : ↑f y ∈ lowerCentralSeries H (Nat.succ d)
⊢ (↑f y)⁻¹ ∈ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
exact Subgroup.inv_mem _ hy
[GOAL]
case succ.intro.intro
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
⊢ ∀ (x : G),
    x ∈ {g | ∃ g₁, g₁ ∈ lowerCentralSeries G d ∧ ∃ g₂, g₂ ∈ ⊤ ∧ ⁅g₁, g₂⁆ = g} → ↑f x ∈ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
rintro a ⟨y, hy, z, ⟨-, rfl⟩⟩
[GOAL]
case succ.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
y : G
hy : y ∈ lowerCentralSeries G d
z : G
⊢ ↑f ⁅y, z⁆ ∈ lowerCentralSeries H (Nat.succ d)
[PROOFSTEP]
apply mem_closure.mpr
[GOAL]
case succ.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
y : G
hy : y ∈ lowerCentralSeries G d
z : G
⊢ ∀ (K : Subgroup H), {g | ∃ g₁, g₁ ∈ lowerCentralSeries H d ∧ ∃ g₂, g₂ ∈ ⊤ ∧ ⁅g₁, g₂⁆ = g} ⊆ ↑K → ↑f ⁅y, z⁆ ∈ K
[PROOFSTEP]
exact fun K hK => hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutatorElement_def]⟩
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
x : G
hx : x ∈ lowerCentralSeries G (Nat.succ d)
y : G
hy : y ∈ lowerCentralSeries G d
z : G
K : Subgroup H
hK : {g | ∃ g₁, g₁ ∈ lowerCentralSeries H d ∧ ∃ g₂, g₂ ∈ ⊤ ∧ ⁅g₁, g₂⁆ = g} ⊆ ↑K
⊢ ∃ g₂, g₂ ∈ ⊤ ∧ ⁅↑f y, g₂⁆ = ↑f ⁅y, z⁆
[PROOFSTEP]
simp [commutatorElement_def]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ lowerCentralSeries G (n + 1) = ⊥
[PROOFSTEP]
rw [lowerCentralSeries_succ, closure_eq_bot_iff, Set.subset_singleton_iff]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ ∀ (y : G), y ∈ {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x} → y = 1
[PROOFSTEP]
rintro x ⟨y, hy1, z, ⟨⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ y * z * y⁻¹ * z⁻¹ = 1
[PROOFSTEP]
rw [mul_assoc, ← mul_inv_rev, mul_inv_eq_one, eq_comm]
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ z * y = y * z
[PROOFSTEP]
exact mem_center_iff.mp (h hy1) z
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
⊢ Group.IsNilpotent G
[PROOFSTEP]
rw [nilpotent_iff_lowerCentralSeries] at *
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : ∃ n, lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥
[PROOFSTEP]
rcases hH with ⟨n, hn⟩
[GOAL]
case intro
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥
[PROOFSTEP]
use n + 1
[GOAL]
case h
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ lowerCentralSeries G (n + 1) = ⊥
[PROOFSTEP]
refine' lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp _) hf1)
[GOAL]
case h
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ Subgroup.map f (lowerCentralSeries G n) = ⊥
[PROOFSTEP]
exact eq_bot_iff.mpr (hn ▸ lowerCentralSeries.map f n)
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
[PROOFSTEP]
haveI : IsNilpotent G := isNilpotent_of_ker_le_center f hf1 hH
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
this : Group.IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
[PROOFSTEP]
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  -- Porting note: Lean needs to be told that predicates are decidable
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
this : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) ≤ nilpotencyClass H + 1
[PROOFSTEP]
refine @Nat.find_min' _ (Classical.decPred _) _ _ ?_
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
this : Group.IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass H + 1) = ⊥
[PROOFSTEP]
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
this : Group.IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥
[PROOFSTEP]
apply eq_bot_iff.mpr
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
this : Group.IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥
[PROOFSTEP]
apply le_trans (lowerCentralSeries.map f _)
[GOAL]
G : Type u_1
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
this : Group.IsNilpotent G
⊢ lowerCentralSeries H (nilpotencyClass H) ≤ ⊥
[PROOFSTEP]
simp only [lowerCentralSeries_nilpotencyClass, le_bot_iff]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
h : Group.IsNilpotent G
f : G →* G'
hf : Function.Surjective ↑f
⊢ Group.IsNilpotent G'
[PROOFSTEP]
rcases h with ⟨n, hn⟩
[GOAL]
case mk.intro
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Group.IsNilpotent G'
[PROOFSTEP]
use n
[GOAL]
case h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤
[PROOFSTEP]
apply eq_top_iff.mpr
[GOAL]
case h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n
[PROOFSTEP]
calc
  ⊤ = f.range := symm (f.range_top_of_surjective hf)
  _ = Subgroup.map f ⊤ := (MonoidHom.range_eq_map _)
  _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
  _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Subgroup.map f ⊤ = Subgroup.map f (upperCentralSeries G n)
[PROOFSTEP]
rw [hn]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
h : Group.IsNilpotent G
⊢ nilpotencyClass G' ≤ nilpotencyClass G
[PROOFSTEP]
refine @Nat.find_mono _ _ (Classical.decPred _) (Classical.decPred _) ?_ _ _
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
h : Group.IsNilpotent G
⊢ ∀ (n : ℕ), upperCentralSeries G n = ⊤ → upperCentralSeries G' n = ⊤
[PROOFSTEP]
intro n hn
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
h : Group.IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤
[PROOFSTEP]
apply eq_top_iff.mpr
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
h : Group.IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n
[PROOFSTEP]
calc
  ⊤ = f.range := symm (f.range_top_of_surjective hf)
  _ = Subgroup.map f ⊤ := (MonoidHom.range_eq_map _)
  _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
  _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
h : Group.IsNilpotent G
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Subgroup.map f ⊤ = Subgroup.map f (upperCentralSeries G n)
[PROOFSTEP]
rw [hn]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
H₁ H₂ : Subgroup G
inst✝¹ : Normal H₁
inst✝ : Normal H₂
h : H₁ = H₂
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂))
[PROOFSTEP]
subst h
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
H₁ : Subgroup G
inst✝¹ inst✝ : Normal H₁
⊢ comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₁) (center (G ⧸ H₁))
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) Nat.zero) = upperCentralSeries G (Nat.succ Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk', (upperCentralSeries_one G).symm]
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (Nat.succ n)) = upperCentralSeries G (Nat.succ (Nat.succ n))
[PROOFSTEP]
let Hn := upperCentralSeries (G ⧸ center G) n
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (Nat.succ n)) = upperCentralSeries G (Nat.succ (Nat.succ n))
[PROOFSTEP]
calc
  comap (mk' (center G)) (upperCentralSeriesStep Hn) =
      comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) :=
    by rw [upperCentralSeriesStep_eq_comap_center]
  _ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
    QuotientGroup.comap_comap_center
  _ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) := (comap_center_subst ih)
  _ = upperCentralSeriesStep (upperCentralSeries G n.succ) := symm (upperCentralSeriesStep_eq_comap_center _)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeriesStep Hn) =
    comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn)))
[PROOFSTEP]
rw [upperCentralSeriesStep_eq_comap_center]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
inst✝ : Group.IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
[PROOFSTEP]
rw [Group.nilpotencyClass, @Nat.find_eq_zero _ (Classical.decPred _), upperCentralSeries_zero,
  subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1
[PROOFSTEP]
generalize hn : Group.nilpotencyClass G = n
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass (G ⧸ center G) = n - 1
[PROOFSTEP]
rcases n with (rfl | n)
[GOAL]
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
hn : nilpotencyClass G = Nat.zero
⊢ nilpotencyClass (G ⧸ center G) = Nat.zero - 1
[PROOFSTEP]
simp [nilpotencyClass_zero_iff_subsingleton] at *
[GOAL]
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton (G ⧸ center G)
[PROOFSTEP]
exact Quotient.instSubsingletonQuotient (leftRel (center G))
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) = Nat.succ n - 1
[PROOFSTEP]
suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
this : nilpotencyClass (G ⧸ center G) = n
⊢ nilpotencyClass (G ⧸ center G) = Nat.succ n - 1
[PROOFSTEP]
simpa
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) = n
[PROOFSTEP]
apply le_antisymm
[GOAL]
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) ≤ n
[PROOFSTEP]
apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
[GOAL]
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ upperCentralSeries (G ⧸ center G) n = ⊤
[PROOFSTEP]
apply @comap_injective G _ _ _ (mk' (center G)) (surjective_quot_mk _)
[GOAL]
case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = comap (mk' (center G)) ⊤
[PROOFSTEP]
rw [comap_upperCentralSeries_quotient_center, comap_top, ← hn]
[GOAL]
case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤
[PROOFSTEP]
exact upperCentralSeries_nilpotencyClass
[GOAL]
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ n ≤ nilpotencyClass (G ⧸ center G)
[PROOFSTEP]
apply le_of_add_le_add_right
[GOAL]
case succ.a.bc
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ n + ?succ.a.a ≤ nilpotencyClass (G ⧸ center G) + ?succ.a.a
case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ ℕ
[PROOFSTEP]
calc
  n + 1 = n.succ := rfl
  _ = Group.nilpotencyClass G := (symm hn)
  _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 := nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _)) _
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass (G ⧸ center G) + 1
[PROOFSTEP]
rw [nilpotencyClass_quotient_center]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1
[PROOFSTEP]
rcases h : Group.nilpotencyClass G with ⟨⟩
[GOAL]
case zero
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = Nat.zero
⊢ Nat.zero = Nat.zero - 1 + 1
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = Nat.zero
⊢ False
[PROOFSTEP]
rw [nilpotencyClass_zero_iff_subsingleton] at h
[GOAL]
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False
[PROOFSTEP]
skip
[GOAL]
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False
[PROOFSTEP]
apply false_of_nontrivial_of_subsingleton G
[GOAL]
case succ
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = Nat.succ n✝
⊢ Nat.succ n✝ = Nat.succ n✝ - 1 + 1
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent (G ⧸ center G)
⊢ Group.IsNilpotent G
[PROOFSTEP]
obtain ⟨n, hn⟩ := h.nilpotent
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ Group.IsNilpotent G
[PROOFSTEP]
use n.succ
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent (G ⧸ center G)
n : ℕ
hn : upperCentralSeries (G ⧸ center G) n = ⊤
⊢ upperCentralSeries G (Nat.succ n) = ⊤
[PROOFSTEP]
simp [← comap_upperCentralSeries_quotient_center, hn]
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
H : Subgroup G✝
inst✝² : Normal H
P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop
G : Type u_2
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ center G) → P G
⊢ P G
[PROOFSTEP]
obtain ⟨n, h⟩ : ∃ n, Group.nilpotencyClass G = n := ⟨_, rfl⟩
[GOAL]
case intro
G✝ : Type u_1
inst✝³ : Group G✝
H : Subgroup G✝
inst✝² : Normal H
P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop
G : Type u_2
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
h : nilpotencyClass G = n
⊢ P G
[PROOFSTEP]
induction' n with n ih generalizing G
[GOAL]
case intro.zero
G✝¹ : Type u_1
inst✝⁵ : Group G✝¹
H : Subgroup G✝¹
inst✝⁴ : Normal H
P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop
G✝ : Type u_2
inst✝³ : Group G✝
inst✝² : Group.IsNilpotent G✝
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
h✝ : nilpotencyClass G✝ = n
G : Type u_2
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G = Nat.zero
⊢ P G
[PROOFSTEP]
haveI := nilpotencyClass_zero_iff_subsingleton.mp h
[GOAL]
case intro.zero
G✝¹ : Type u_1
inst✝⁵ : Group G✝¹
H : Subgroup G✝¹
inst✝⁴ : Normal H
P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop
G✝ : Type u_2
inst✝³ : Group G✝
inst✝² : Group.IsNilpotent G✝
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
h✝ : nilpotencyClass G✝ = n
G : Type u_2
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G = Nat.zero
this : Subsingleton G
⊢ P G
[PROOFSTEP]
exact hbase _
[GOAL]
case intro.succ
G✝¹ : Type u_1
inst✝⁵ : Group G✝¹
H : Subgroup G✝¹
inst✝⁴ : Normal H
P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop
G✝ : Type u_2
inst✝³ : Group G✝
inst✝² : Group.IsNilpotent G✝
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ center G) → P G
n✝ : ℕ
h✝ : nilpotencyClass G✝ = n✝
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G = Nat.succ n
⊢ P G
[PROOFSTEP]
have hn : Group.nilpotencyClass (G ⧸ center G) = n := by simp [nilpotencyClass_quotient_center, h]
[GOAL]
G✝¹ : Type u_1
inst✝⁵ : Group G✝¹
H : Subgroup G✝¹
inst✝⁴ : Normal H
P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop
G✝ : Type u_2
inst✝³ : Group G✝
inst✝² : Group.IsNilpotent G✝
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ center G) → P G
n✝ : ℕ
h✝ : nilpotencyClass G✝ = n✝
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) = n
[PROOFSTEP]
simp [nilpotencyClass_quotient_center, h]
[GOAL]
case intro.succ
G✝¹ : Type u_1
inst✝⁵ : Group G✝¹
H : Subgroup G✝¹
inst✝⁴ : Normal H
P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop
G✝ : Type u_2
inst✝³ : Group G✝
inst✝² : Group.IsNilpotent G✝
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ center G) → P G
n✝ : ℕ
h✝ : nilpotencyClass G✝ = n✝
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G = Nat.succ n
hn : nilpotencyClass (G ⧸ center G) = n
⊢ P G
[PROOFSTEP]
exact hstep _ (ih _ hn)
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
⊢ derivedSeries G n ≤ lowerCentralSeries G n
[PROOFSTEP]
induction' n with i ih
[GOAL]
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ derivedSeries G Nat.zero ≤ lowerCentralSeries G Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
i : ℕ
ih : derivedSeries G i ≤ lowerCentralSeries G i
⊢ derivedSeries G (Nat.succ i) ≤ lowerCentralSeries G (Nat.succ i)
[PROOFSTEP]
apply commutator_mono ih
[GOAL]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
i : ℕ
ih : derivedSeries G i ≤ lowerCentralSeries G i
⊢ derivedSeries G i ≤ ⊤
[PROOFSTEP]
simp
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_2
inst✝ : CommGroup G
⊢ Group.IsNilpotent G
[PROOFSTEP]
use 1
[GOAL]
case h
G✝ : Type u_1
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_2
inst✝ : CommGroup G
⊢ upperCentralSeries G 1 = ⊤
[PROOFSTEP]
rw [upperCentralSeries_one]
[GOAL]
case h
G✝ : Type u_1
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤
[PROOFSTEP]
apply CommGroup.center_eq_top
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_2
inst✝ : CommGroup G
⊢ nilpotencyClass G ≤ 1
[PROOFSTEP]
apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_2
inst✝ : CommGroup G
⊢ upperCentralSeries G 1 = ⊤
[PROOFSTEP]
rw [upperCentralSeries_one]
[GOAL]
G✝ : Type u_1
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤
[PROOFSTEP]
apply CommGroup.center_eq_top
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ center G = ⊤
[PROOFSTEP]
rw [← upperCentralSeries_one]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
inst✝ : Group.IsNilpotent G
h : nilpotencyClass G ≤ 1
⊢ upperCentralSeries G 1 = ⊤
[PROOFSTEP]
exact upperCentralSeries_eq_top_iff_nilpotencyClass_le.mpr h
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
⊢ lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
⊢ lowerCentralSeries (G₁ × G₂) Nat.zero = prod (lowerCentralSeries G₁ Nat.zero) (lowerCentralSeries G₂ Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
⊢ lowerCentralSeries (G₁ × G₂) (Nat.succ n) =
    prod (lowerCentralSeries G₁ (Nat.succ n)) (lowerCentralSeries G₂ (Nat.succ n))
[PROOFSTEP]
calc
  lowerCentralSeries (G₁ × G₂) n.succ = ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ := rfl
  _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), ⊤⁆ := by rw [ih]
  _ = ⁅(lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n), (⊤ : Subgroup G₁).prod ⊤⁆ := by simp
  _ = ⁅lowerCentralSeries G₁ n, (⊤ : Subgroup G₁)⁆.prod ⁅lowerCentralSeries G₂ n, ⊤⁆ := (commutator_prod_prod _ _ _ _)
  _ = (lowerCentralSeries G₁ n.succ).prod (lowerCentralSeries G₂ n.succ) := rfl
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
⊢ ⁅lowerCentralSeries (G₁ × G₂) n, ⊤⁆ = ⁅prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n), ⊤⁆
[PROOFSTEP]
rw [ih]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
n : ℕ
ih : lowerCentralSeries (G₁ × G₂) n = prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n)
⊢ ⁅prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n), ⊤⁆ =
    ⁅prod (lowerCentralSeries G₁ n) (lowerCentralSeries G₂ n), prod ⊤ ⊤⁆
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
⊢ Group.IsNilpotent (G₁ × G₂)
[PROOFSTEP]
rw [nilpotent_iff_lowerCentralSeries]
[GOAL]
G : Type u_1
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
⊢ ∃ n, lowerCentralSeries (G₁ × G₂) n = ⊥
[PROOFSTEP]
refine' ⟨max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂), _⟩
[GOAL]
G : Type u_1
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
⊢ lowerCentralSeries (G₁ × G₂) (max (nilpotencyClass G₁) (nilpotencyClass G₂)) = ⊥
[PROOFSTEP]
rw [lowerCentralSeries_prod, lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_left _ _),
  lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (le_max_right _ _), bot_prod_bot]
[GOAL]
G : Type u_1
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
⊢ nilpotencyClass (G₁ × G₂) = max (nilpotencyClass G₁) (nilpotencyClass G₂)
[PROOFSTEP]
refine' eq_of_forall_ge_iff fun k => _
[GOAL]
G : Type u_1
inst✝⁵ : Group G
H : Subgroup G
inst✝⁴ : Normal H
G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : Group.IsNilpotent G₁
inst✝ : Group.IsNilpotent G₂
k : ℕ
⊢ nilpotencyClass (G₁ × G₂) ≤ k ↔ max (nilpotencyClass G₁) (nilpotencyClass G₂) ≤ k
[PROOFSTEP]
simp only [max_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, lowerCentralSeries_prod, prod_eq_bot_iff]
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ pi Set.univ fun i => lowerCentralSeries (Gs i) n
[PROOFSTEP]
let pi := fun f : ∀ i, Subgroup (Gs i) => Subgroup.pi Set.univ f
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) Nat.zero ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) Nat.zero
[PROOFSTEP]
simp [pi_top]
[GOAL]
case succ
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ lowerCentralSeries ((i : η) → Gs i) (Nat.succ n) ≤
    Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) (Nat.succ n)
[PROOFSTEP]
calc
  lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
  _ ≤ ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_mono ih (le_refl _))
  _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆ := by simp [pi_top]
  _ ≤ pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_pi_pi_le _ _)
  _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
[GOAL]
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆
[PROOFSTEP]
simp [pi_top]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ Group.IsNilpotent ((i : η) → Gs i)
[PROOFSTEP]
rw [nilpotent_iff_lowerCentralSeries]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∃ n, lowerCentralSeries ((i : η) → Gs i) n = ⊥
[PROOFSTEP]
refine' ⟨n, _⟩
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ lowerCentralSeries ((i : η) → Gs i) n ≤ ⊥
[PROOFSTEP]
apply le_trans (lowerCentralSeries_pi_le _)
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ (pi Set.univ fun i => lowerCentralSeries (Gs i) n) ≤ ⊥
[PROOFSTEP]
rw [← eq_bot_iff, pi_eq_bot_iff]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
⊢ ∀ (i : η), lowerCentralSeries (Gs i) n = ⊥
[PROOFSTEP]
intro i
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
n : ℕ
h : ∀ (i : η), nilpotencyClass (Gs i) ≤ n
i : η
⊢ lowerCentralSeries (Gs i) n = ⊥
[PROOFSTEP]
apply lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr (h i)
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
n : ℕ
⊢ lowerCentralSeries ((i : η) → Gs i) n = pi Set.univ fun i => lowerCentralSeries (Gs i) n
[PROOFSTEP]
let pi := fun f : ∀ i, Subgroup (Gs i) => Subgroup.pi Set.univ f
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
n : ℕ
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) n = Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
⊢ lowerCentralSeries ((i : η) → Gs i) Nat.zero = Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) Nat.zero
[PROOFSTEP]
simp [pi_top]
[GOAL]
case succ
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n = Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ lowerCentralSeries ((i : η) → Gs i) (Nat.succ n) =
    Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) (Nat.succ n)
[PROOFSTEP]
calc
  lowerCentralSeries (∀ i, Gs i) n.succ = ⁅lowerCentralSeries (∀ i, Gs i) n, ⊤⁆ := rfl
  _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ := by rw [ih]
  _ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆ := by simp [pi_top]
  _ = pi fun i => ⁅lowerCentralSeries (Gs i) n, ⊤⁆ := (commutator_pi_pi_of_finite _ _)
  _ = pi fun i => lowerCentralSeries (Gs i) n.succ := rfl
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n = Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ ⁅lowerCentralSeries ((i : η) → Gs i) n, ⊤⁆ = ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆
[PROOFSTEP]
rw [ih]
[GOAL]
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
pi : ((i : η) → Subgroup (Gs i)) → Subgroup ((i : η) → Gs i) := fun f => Subgroup.pi Set.univ f
n : ℕ
ih : lowerCentralSeries ((i : η) → Gs i) n = Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
⊢ ⁅pi fun i => lowerCentralSeries (Gs i) n, ⊤⁆ = ⁅pi fun i => lowerCentralSeries (Gs i) n, pi fun i => ⊤⁆
[PROOFSTEP]
simp [pi_top]
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
⊢ Group.IsNilpotent ((i : η) → Gs i)
[PROOFSTEP]
cases nonempty_fintype η
[GOAL]
case intro
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
val✝ : Fintype η
⊢ Group.IsNilpotent ((i : η) → Gs i)
[PROOFSTEP]
rw [nilpotent_iff_lowerCentralSeries]
[GOAL]
case intro
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∃ n, lowerCentralSeries ((i : η) → Gs i) n = ⊥
[PROOFSTEP]
refine' ⟨Finset.univ.sup fun i => Group.nilpotencyClass (Gs i), _⟩
[GOAL]
case intro
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
val✝ : Fintype η
⊢ lowerCentralSeries ((i : η) → Gs i) (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) = ⊥
[PROOFSTEP]
rw [lowerCentralSeries_pi_of_finite, pi_eq_bot_iff]
[GOAL]
case intro
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
val✝ : Fintype η
⊢ ∀ (i : η), lowerCentralSeries (Gs i) (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) = ⊥
[PROOFSTEP]
intro i
[GOAL]
case intro
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
val✝ : Fintype η
i : η
⊢ lowerCentralSeries (Gs i) (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) = ⊥
[PROOFSTEP]
apply lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr
[GOAL]
case intro
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Finite η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
val✝ : Fintype η
i : η
⊢ nilpotencyClass (Gs i) ≤ Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)
[PROOFSTEP]
exact @Finset.le_sup _ _ _ _ Finset.univ (fun i => Group.nilpotencyClass (Gs i)) _ (Finset.mem_univ i)
[GOAL]
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
⊢ nilpotencyClass ((i : η) → Gs i) = Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)
[PROOFSTEP]
apply eq_of_forall_ge_iff
[GOAL]
case H
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
⊢ ∀ (c : ℕ), nilpotencyClass ((i : η) → Gs i) ≤ c ↔ (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) ≤ c
[PROOFSTEP]
intro k
[GOAL]
case H
G : Type u_1
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : Normal H
η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)
k : ℕ
⊢ nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.sup Finset.univ fun i => nilpotencyClass (Gs i)) ≤ k
[PROOFSTEP]
simp only [Finset.sup_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le, lowerCentralSeries_pi_of_finite,
  pi_eq_bot_iff, Finset.mem_univ, true_imp_iff]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ IsSolvable G
[PROOFSTEP]
obtain ⟨n, hn⟩ := nilpotent_iff_lowerCentralSeries.1 h
[GOAL]
case intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ IsSolvable G
[PROOFSTEP]
use n
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ derivedSeries G n = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← hn]
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
n : ℕ
hn : lowerCentralSeries G n = ⊥
⊢ derivedSeries G n ≤ lowerCentralSeries G n
[PROOFSTEP]
exact derived_le_lower_central n
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ NormalizerCondition G
[PROOFSTEP]
rw [normalizerCondition_iff_only_full_group_self_normalizing]
[GOAL]
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ ∀ (H : Subgroup G), normalizer H = H → H = ⊤
[PROOFSTEP]
apply @nilpotent_center_quotient_ind _ G _ _
[GOAL]
case hbase
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Subsingleton G] (H : Subgroup G), normalizer H = H → H = ⊤
[PROOFSTEP]
clear! G
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
h : Group.IsNilpotent G
⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Group.IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer H = H → H = ⊤
[PROOFSTEP]
clear! G
[GOAL]
case hbase
⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Subsingleton G] (H : Subgroup G), normalizer H = H → H = ⊤
[PROOFSTEP]
intro G _ _ H _
[GOAL]
case hbase
G : Type u_1
inst✝¹ : Group G
inst✝ : Subsingleton G
H : Subgroup G
a✝ : normalizer H = H
⊢ H = ⊤
[PROOFSTEP]
exact @Subsingleton.elim _ Unique.instSubsingleton _ _
[GOAL]
case hstep
⊢ ∀ (G : Type u_1) [inst : Group G] [inst_1 : Group.IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer H = H → H = ⊤
[PROOFSTEP]
intro G _ _ ih H hH
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
⊢ H = ⊤
[PROOFSTEP]
have hch : center G ≤ H := Subgroup.center_le_normalizer.trans (le_of_eq hH)
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
⊢ H = ⊤
[PROOFSTEP]
have hkh : (mk' (center G)).ker ≤ H := by simpa using hch
[GOAL]
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
⊢ MonoidHom.ker (mk' (center G)) ≤ H
[PROOFSTEP]
simpa using hch
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
⊢ H = ⊤
[PROOFSTEP]
have hsur : Function.Surjective (mk' (center G)) := surjective_quot_mk _
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
⊢ H = ⊤
[PROOFSTEP]
let H' := H.map (mk' (center G))
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ H = ⊤
[PROOFSTEP]
have hH' : H'.normalizer = H' := by
  apply comap_injective hsur
  rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
  exact hH
[GOAL]
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer H' = H'
[PROOFSTEP]
apply comap_injective hsur
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ comap (mk' (center G)) (normalizer H') = comap (mk' (center G)) H'
[PROOFSTEP]
rw [comap_normalizer_eq_of_surjective _ hsur, comap_map_eq_self hkh]
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
⊢ normalizer H = H
[PROOFSTEP]
exact hH
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : normalizer H' = H'
⊢ H = ⊤
[PROOFSTEP]
apply map_injective_of_ker_le (mk' (center G)) hkh le_top
[GOAL]
case hstep
G : Type u_1
inst✝¹ : Group G
inst✝ : Group.IsNilpotent G
ih : ∀ (H : Subgroup (G ⧸ center G)), normalizer H = H → H = ⊤
H : Subgroup G
hH : normalizer H = H
hch : center G ≤ H
hkh : MonoidHom.ker (mk' (center G)) ≤ H
hsur : Function.Surjective ↑(mk' (center G))
H' : Subgroup (G ⧸ center G) := Subgroup.map (mk' (center G)) H
hH' : normalizer H' = H'
⊢ Subgroup.map (mk' (center G)) H = Subgroup.map (mk' (center G)) ⊤
[PROOFSTEP]
exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur))
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
⊢ Group.IsNilpotent G
[PROOFSTEP]
cases' nonempty_fintype G
[GOAL]
case intro
G : Type u_1
hG : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val✝ : Fintype G
⊢ Group.IsNilpotent G
[PROOFSTEP]
classical
revert hG
apply @Fintype.induction_subsingleton_or_nontrivial _ G _
· intro _ _ _ _
  infer_instance
· intro G _ _ ih _ h
  have hcq : Fintype.card (G ⧸ center G) < Fintype.card G :=
    by
    rw [card_eq_card_quotient_mul_card_subgroup (center G)]
    apply lt_mul_of_one_lt_right
    exact Fintype.card_pos_iff.mpr One.nonempty
    exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
  have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
  exact of_quotient_center_nilpotent hnq
[GOAL]
case intro
G : Type u_1
hG : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
h : IsPGroup p G
val✝ : Fintype G
⊢ Group.IsNilpotent G
[PROOFSTEP]
revert hG
[GOAL]
case intro
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ [hG : Group G], IsPGroup p G → Group.IsNilpotent G
[PROOFSTEP]
apply @Fintype.induction_subsingleton_or_nontrivial _ G _
[GOAL]
case intro.hbase
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ (α : Type u_1) [inst : Fintype α] [inst : Subsingleton α] [hG : Group α], IsPGroup p α → Group.IsNilpotent α
[PROOFSTEP]
intro _ _ _ _
[GOAL]
case intro.hbase
G : Type u_1
inst✝² : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
α✝ : Type u_1
inst✝¹ : Fintype α✝
inst✝ : Subsingleton α✝
hG✝ : Group α✝
⊢ IsPGroup p α✝ → Group.IsNilpotent α✝
[PROOFSTEP]
infer_instance
[GOAL]
case intro.hstep
G : Type u_1
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : Nontrivial α],
    (∀ (β : Type u_1) [inst_2 : Fintype β], card β < card α → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β) →
      ∀ [hG : Group α], IsPGroup p α → Group.IsNilpotent α
[PROOFSTEP]
intro G _ _ ih _ h
[GOAL]
case intro.hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ Group.IsNilpotent G
[PROOFSTEP]
have hcq : Fintype.card (G ⧸ center G) < Fintype.card G :=
  by
  rw [card_eq_card_quotient_mul_card_subgroup (center G)]
  apply lt_mul_of_one_lt_right
  exact Fintype.card_pos_iff.mpr One.nonempty
  exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
[GOAL]
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card G
[PROOFSTEP]
rw [card_eq_card_quotient_mul_card_subgroup (center G)]
[GOAL]
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ card (G ⧸ center G) < card (G ⧸ center G) * card { x // x ∈ center G }
[PROOFSTEP]
apply lt_mul_of_one_lt_right
[GOAL]
case ha
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 0 < card (G ⧸ center G)
case h
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card { x // x ∈ center G }
[PROOFSTEP]
exact Fintype.card_pos_iff.mpr One.nonempty
[GOAL]
case h
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
⊢ 1 < card { x // x ∈ center G }
[PROOFSTEP]
exact (Subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)
[GOAL]
case intro.hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
⊢ Group.IsNilpotent G
[PROOFSTEP]
have hnq : IsNilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G))
[GOAL]
case intro.hstep
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
val✝ : Fintype G✝
G : Type u_1
inst✝¹ : Fintype G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [inst : Fintype β], card β < card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG✝ : Group G
h : IsPGroup p G
hcq : card (G ⧸ center G) < card G
hnq : Group.IsNilpotent (G ⧸ center G)
⊢ Group.IsNilpotent G
[PROOFSTEP]
exact of_quotient_center_nilpotent hnq
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
⊢ Group.IsNilpotent G
[PROOFSTEP]
classical
let ps := (Fintype.card G).factorization.support
have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) :=
  by
  intro p P
  haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p))
  exact P.isPGroup'.isNilpotent
exact nilpotent_of_mulEquiv e
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
⊢ Group.IsNilpotent G
[PROOFSTEP]
let ps := (Fintype.card G).factorization.support
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
⊢ Group.IsNilpotent G
[PROOFSTEP]
have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) :=
  by
  intro p P
  haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p))
  exact P.isPGroup'.isNilpotent
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
⊢ ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), Group.IsNilpotent { x // x ∈ ↑P }
[PROOFSTEP]
intro p P
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
p : { x // x ∈ ps }
P : Sylow (↑p) G
⊢ Group.IsNilpotent { x // x ∈ ↑P }
[PROOFSTEP]
haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p))
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
p : { x // x ∈ ps }
P : Sylow (↑p) G
this : Fact (Nat.Prime ↑p)
⊢ Group.IsNilpotent { x // x ∈ ↑P }
[PROOFSTEP]
exact P.isPGroup'.isNilpotent
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
this : ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), Group.IsNilpotent { x // x ∈ ↑P }
⊢ Group.IsNilpotent G
[PROOFSTEP]
exact nilpotent_of_mulEquiv e
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
[PROOFSTEP]
tfae_have 1 → 2
[GOAL]
case tfae_1_to_2
G : Type u_1
hG : Group G
inst✝ : Fintype G
⊢ Group.IsNilpotent G → NormalizerCondition G
[PROOFSTEP]
exact @normalizerCondition_of_isNilpotent _ _
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
⊢ NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
[PROOFSTEP]
exact fun h H => NormalizerCondition.normal_of_coatom H h
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
[PROOFSTEP]
tfae_have 3 → 4
[GOAL]
case tfae_3_to_4
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
⊢ (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
[PROOFSTEP]
intro h p _ P
[GOAL]
case tfae_3_to_4
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
h : ∀ (H : Subgroup G), IsCoatom H → Normal H
p : ℕ
_hp✝ : Fact (Nat.Prime p)
P : Sylow p G
⊢ Normal ↑P
[PROOFSTEP]
exact Sylow.normal_of_all_max_subgroups_normal h _
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
[PROOFSTEP]
tfae_have 4 → 5
[GOAL]
case tfae_4_to_5
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
⊢ (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
[PROOFSTEP]
exact fun h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP)
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
[PROOFSTEP]
tfae_have 5 → 1
[GOAL]
case tfae_5_to_1
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
⊢ Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G) →
    Group.IsNilpotent G
[PROOFSTEP]
rintro ⟨e⟩
[GOAL]
case tfae_5_to_1.intro
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
⊢ Group.IsNilpotent G
[PROOFSTEP]
exact isNilpotent_of_product_of_sylow_group e
[GOAL]
G : Type u_1
hG : Group G
inst✝ : Fintype G
tfae_1_to_2 : Group.IsNilpotent G → NormalizerCondition G
tfae_2_to_3 : NormalizerCondition G → ∀ (H : Subgroup G), IsCoatom H → Normal H
tfae_3_to_4 : (∀ (H : Subgroup G), IsCoatom H → Normal H) → ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P
tfae_4_to_5 :
  (∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P) →
    Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)
tfae_5_to_1 :
  Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G) →
    Group.IsNilpotent G
⊢ List.TFAE
    [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → Normal H,
      ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), Normal ↑P,
      Nonempty (((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G)]
[PROOFSTEP]
tfae_finish