case zero
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
⊢ Subgroup.map f (upperCentralSeries G Nat.zero) ≤ upperCentralSeries H Nat.zero

case succ
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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)
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
n : ℕ
⊢ Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n
induction' n with d hd
no goals
case zero
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
h : Function.Surjective ↑f
⊢ Subgroup.map f (upperCentralSeries G Nat.zero) ≤ upperCentralSeries H Nat.zero
simp
case succ.intro.intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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
case succ
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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)
rintro _ ⟨x, hx : x ∈ upperCentralSeries G d.succ, rfl⟩ y'
case succ.intro.intro.intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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
case succ.intro.intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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
rcases h y' with ⟨y, rfl⟩
no goals
case succ.intro.intro.intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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
simpa using hd (mem_map_of_mem f (hx y))