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

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

Tactic:
obtain ⟨h0, hH⟩ := hasc

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 + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
⊢ IsDescendingCentralSeries 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 + 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)

Tactic:
dsimp 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 + 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)

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

Tactic:
group

Result:
no goals

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

Tactic:
convert hx 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 + 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)

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 + 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)

Tactic:
subst hx

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 + 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)

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 + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
⊢ IsDescendingCentralSeries 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 + 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)

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 + 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)

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

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 + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ 1 ∈ (fun m => H (n - m)) (m + 1)

Tactic:
exact Subgroup.one_mem _

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 + 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)

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 + 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)

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 + 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)

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 + 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)

Tactic:
apply hH

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

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 + 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)

Tactic:
rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx

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 + 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)

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 + 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)

Tactic:
rw [show (1 : G) * g * (1⁻¹ : G) * g⁻¹ = 1 by group]

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 + 1) → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ H n
m : ℕ
g : G
hm : n ≤ m
⊢ 1 ∈ (fun m => H (n - m)) (m + 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 + 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)

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 + 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)