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
⊢ Subgroup.map f (lowerCentralSeries G Nat.zero) ≤ lowerCentralSeries 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
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
⊢ Subgroup.map f (lowerCentralSeries G (Nat.succ d)) ≤ lowerCentralSeries 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
n : ℕ
⊢ Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries 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
⊢ Subgroup.map f (lowerCentralSeries G Nat.zero) ≤ lowerCentralSeries H Nat.zero
simp [Nat.zero_eq]
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
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)
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
d : ℕ
hd : Subgroup.map f (lowerCentralSeries G d) ≤ lowerCentralSeries H d
⊢ Subgroup.map f (lowerCentralSeries G (Nat.succ d)) ≤ lowerCentralSeries H (Nat.succ d)
rintro a ⟨x, hx : x ∈ lowerCentralSeries G d.succ, rfl⟩
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
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)
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
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)
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)
case succ.intro.intro.intro.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
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)
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
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)
rintro a ⟨y, hy, z, ⟨-, rfl⟩⟩
case succ.intro.intro.intro.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
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
case succ.intro.intro.intro.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
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)
apply mem_closure.mpr
no goals
case succ.intro.intro.intro.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
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
exact fun K hK => hK ⟨f y, hd (mem_map_of_mem f hy), by simp [commutatorElement_def]⟩
no goals
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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)
simp [f.map_one, Subgroup.one_mem _]
no goals
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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)
simp [MonoidHom.map_mul, Subgroup.mul_mem _ hy hz]
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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)
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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)
rw [f.map_inv]
no goals
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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)
exact Subgroup.inv_mem _ hy
no goals
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
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⁆
simp [commutatorElement_def]