case mk.intro
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Group.IsNilpotent G'
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
h : Group.IsNilpotent G
f : G →* G'
hf : Function.Surjective ↑f
⊢ Group.IsNilpotent G'
rcases h with ⟨n, hn⟩
case mk.intro
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤
case mk.intro
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Group.IsNilpotent G'
use n
case mk.intro
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n
case mk.intro
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤
apply eq_top_iff.mpr
no goals
case mk.intro
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n
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
no goals
G : Type u_2
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
G' : Type u_1
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ Subgroup.map f ⊤ = Subgroup.map f (upperCentralSeries G n)
rw [hn]