-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotent_center_quotient_ind {P : ∀ (G) [Group G] [IsNilpotent G], Prop}
    (G : Type*) [Group G] [IsNilpotent G]
    (hbase : ∀ (G) [Group G] [Subsingleton G], P G)
    (hstep : ∀ (G) [Group G] [IsNilpotent G], P (G ⧸ center G) → P G) : P G

Proof state:
case intro.zero
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = 0
this : Subsingleton G
⊢ P G

Tactic:
exact hbase _

Result:
no goals

Proof state:
case intro
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
h : nilpotencyClass G = n
⊢ P G

Tactic:
induction' n with n ih generalizing G

Result:
case intro.zero
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = 0
⊢ P G

case intro.succ
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = n + 1
⊢ P G

Proof state:
case intro.succ
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = n + 1
hn : nilpotencyClass (G ⧸ center G) = n
⊢ P G

Tactic:
exact hstep _ (ih _ hn)

Result:
no goals

Proof state:
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n

Tactic:
simp [nilpotencyClass_quotient_center, h]

Result:
no goals

Proof state:
case intro.succ
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = n + 1
⊢ P G

Tactic:
have hn : Group.nilpotencyClass (G ⧸ center G) = n := by
  simp [nilpotencyClass_quotient_center, h]

Result:
case intro.succ
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
ih : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], nilpotencyClass G = n → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = n + 1
hn : nilpotencyClass (G ⧸ center G) = n
⊢ P G

Proof state:
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
⊢ P G

Tactic:
obtain ⟨n, h⟩ : ∃ n, Group.nilpotencyClass G = n := ⟨_, rfl⟩

Result:
case intro
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
n : ℕ
h : nilpotencyClass G = n
⊢ P G

Proof state:
case intro.zero
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = 0
⊢ P G

Tactic:
haveI := nilpotencyClass_zero_iff_subsingleton.mp h

Result:
case intro.zero
P : (G : Type u_2) → [inst : Group G] → [inst : IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = 0
this : Subsingleton G
⊢ P G