-- Mathlib/GroupTheory/Nilpotent.lean
theorem is_ascending_rev_series_of_is_descending {H : ℕ → Subgroup G} {n : ℕ} (hn : H n = ⊥)
    (hdesc : IsDescendingCentralSeries H) : IsAscendingCentralSeries fun m : ℕ => H (n - m)

Proof state:
case intro
G : Type u_1
inst✝ : Group G
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

Tactic:
dsimp only at hx ⊢

Result:
case intro
G : Type u_1
inst✝ : Group G
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)

Proof state:
case pos
G : Type u_1
inst✝ : Group G
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)

Tactic:
have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm

Result:
case pos
G : Type u_1
inst✝ : Group G
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)

Proof state:
case intro
G : Type u_1
inst✝ : Group G
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)

Tactic:
by_cases hm : n ≤ m

Result:
case pos
G : Type u_1
inst✝ : Group G
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)

case neg
G : Type u_1
inst✝ : Group G
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)

Proof state:
case pos
G : Type u_1
inst✝ : Group G
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⁻¹ ∈ ⊤

Tactic:
exact mem_top _

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : Group G
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)

Tactic:
refine ⟨hn, fun x m hx g => ?_⟩

Result:
case intro
G : Type u_1
inst✝ : Group G
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

Proof state:
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
hdesc : IsDescendingCentralSeries H
⊢ IsAscendingCentralSeries fun m => H (n - m)

Tactic:
obtain ⟨h0, hH⟩ := hdesc

Result:
case intro
G : Type u_1
inst✝ : Group G
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)

Proof state:
case pos
G : Type u_1
inst✝ : Group G
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)

Tactic:
rw [hnm, h0]

Result:
case pos
G : Type u_1
inst✝ : Group G
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⁻¹ ∈ ⊤

Proof state:
case neg
G : Type u_1
inst✝ : Group G
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)

Tactic:
convert hH x _ hx g using 1

Result:
case h.e'_4
G : Type u_1
inst✝ : Group G
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)

Proof state:
case neg
G : Type u_1
inst✝ : Group G
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)

Tactic:
push_neg at hm

Result:
case neg
G : Type u_1
inst✝ : Group G
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)

Proof state:
case h.e'_4
G : Type u_1
inst✝ : Group G
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)

Tactic:
rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]

Result:
no goals