-- Mathlib/GroupTheory/Solvable.lean
theorem isSolvable_iff_commutator_lt [WellFoundedLT (Subgroup G)] :
    IsSolvable G ↔ ∀ H : Subgroup G, H ≠ ⊥ → ⁅H, H⁆ < H

Proof state:
case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
⊢ map H.subtype (derivedSeries (↥H) (0 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)

Tactic:
rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
  ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]

Result:
no goals

Proof state:
case h.succ
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ map H.subtype (derivedSeries (↥H) (n + 1 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))

Tactic:
rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)

Tactic:
induction' n with n ih

Result:
case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
⊢ map H.subtype (derivedSeries (↥H) (0 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)

case h.succ
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ map H.subtype (derivedSeries (↥H) (n + 1 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : derivedSeries (↥⁅H, H⁆) n = ⊥
⊢ derivedSeries (↥H) (n + 1) = ⊥

Tactic:
rw [← (map_injective (subtype_injective _)).eq_iff, Subgroup.map_bot] at hn ⊢

Result:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
⊢ (fun H => IsSolvable ↥H) H

Tactic:
rcases eq_or_ne H ⊥ with rfl | h'

Result:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
hH : ∀ y < ⊥, (fun H => IsSolvable ↥H) y
⊢ IsSolvable ↥⊥

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
⊢ IsSolvable ↥H

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable ↥⊤

Tactic:
refine WellFoundedLT.induction (C := fun (H : Subgroup G) ↦ IsSolvable H) ⊤ fun H hH ↦ ?_

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
⊢ (fun H => IsSolvable ↥H) H

Proof state:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
hH : ∀ y < ⊥, (fun H => IsSolvable ↥H) y
⊢ IsSolvable ↥⊥

Tactic:
infer_instance

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable G

Tactic:
suffices h : IsSolvable (⊤ : Subgroup G) from
  solvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable ↥⊤

Proof state:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
⊢ IsSolvable ↥H

Tactic:
obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')

Result:
case inr.mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : derivedSeries (↥⁅H, H⁆) n = ⊥
⊢ IsSolvable ↥H

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥

Tactic:
rw [← hn]

Result:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
⊢ IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H

Tactic:
refine ⟨fun _ _ ↦ IsSolvable.commutator_lt_of_ne_bot, fun h ↦ ?_⟩

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
⊢ IsSolvable G

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)

Tactic:
clear hn

Result:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)

Proof state:
case inr.mk.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : derivedSeries (↥⁅H, H⁆) n = ⊥
⊢ IsSolvable ↥H

Tactic:
use n + 1

Result:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, (fun H => IsSolvable ↥H) y
h' : H ≠ ⊥
n : ℕ
hn : derivedSeries (↥⁅H, H⁆) n = ⊥
⊢ derivedSeries (↥H) (n + 1) = ⊥