awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) 0) (derivedSeries (↥H) 0)) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₂ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₃ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype ⊤
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₄ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = map ⁅H, H⁆.subtype ⊤
Tactic: rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) 0) (derivedSeries (↥H) 0)) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₂ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₃ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype ⊤
h₄ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = map ⁅H, H⁆.subtype ⊤
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₅ : ⁅H.subtype.range, H.subtype.range⁆ = map ⁅H, H⁆.subtype ⊤
Tactic: rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) 0) (derivedSeries (↥H) 0)) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₂ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₃ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype ⊤
h₄ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = map ⁅H, H⁆.subtype ⊤
h₅ : ⁅H.subtype.range, H.subtype.range⁆ = map ⁅H, H⁆.subtype ⊤
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₆ : ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆.subtype.range
Tactic: rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) 0) (derivedSeries (↥H) 0)) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₂ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₃ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype ⊤
h₄ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = map ⁅H, H⁆.subtype ⊤
h₅ : ⁅H.subtype.range, H.subtype.range⁆ = map ⁅H, H⁆.subtype ⊤
h₆ : ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆.subtype.range
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₇ : ⁅H, H⁆ = ⁅H, H⁆.subtype.range
Tactic: rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) 0) (derivedSeries (↥H) 0)) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₂ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
h₃ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = map ⁅H, H⁆.subtype ⊤
h₄ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = map ⁅H, H⁆.subtype ⊤
h₅ : ⁅H.subtype.range, H.subtype.range⁆ = map ⁅H, H⁆.subtype ⊤
h₆ : ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆.subtype.range
h₇ : ⁅H, H⁆ = ⁅H, H⁆.subtype.range
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₈ : ⁅H, H⁆ = ⁅H, H⁆
Tactic: rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥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))
have h₁ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) (derivedSeries (↥H) (n + 1))) =
  map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
Tactic: rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) (derivedSeries (↥H) (n + 1))) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
⊢ map H.subtype (derivedSeries (↥H) (n + 1 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
have h₂ : ⁅map H.subtype (derivedSeries (↥H) (n + 1)), map H.subtype (derivedSeries (↥H) (n + 1))⁆ =
  map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
Tactic: rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) (derivedSeries (↥H) (n + 1))) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
h₂ :
  ⁅map H.subtype (derivedSeries (↥H) (n + 1)), map H.subtype (derivedSeries (↥H) (n + 1))⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
⊢ map H.subtype (derivedSeries (↥H) (n + 1 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
have h₃ : ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
  map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
Tactic: rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) (derivedSeries (↥H) (n + 1))) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
h₂ :
  ⁅map H.subtype (derivedSeries (↥H) (n + 1)), map H.subtype (derivedSeries (↥H) (n + 1))⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
h₃ :
  ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
⊢ map H.subtype (derivedSeries (↥H) (n + 1 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
have h₄ : ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
  map ⁅H, H⁆.subtype (Bracket.bracket (L := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) (derivedSeries (↥⁅H, H⁆) n))
Tactic: rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
h₁ :
  map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) (derivedSeries (↥H) (n + 1))) =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
h₂ :
  ⁅map H.subtype (derivedSeries (↥H) (n + 1)), map H.subtype (derivedSeries (↥H) (n + 1))⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
h₃ :
  ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
h₄ :
  ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
    map ⁅H, H⁆.subtype (Bracket.bracket (L := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) (derivedSeries (↥⁅H, H⁆) n))
⊢ map H.subtype (derivedSeries (↥H) (n + 1 + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
have h₅ : ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆ =
  ⁅map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n), map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)⁆
Tactic: rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
n : ℕ
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
have h₁ : map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
Tactic: induction n with
    | zero =>
      rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
    | succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable.{u_1} ↥y
h' : H ≠ ⊥
n : ℕ
h₁ : map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
have 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: induction n with
    | zero =>
      rw [derivedSeries_succ, derivedSeries_zero, derivedSeries_zero, map_commutator,
        ← MonoidHom.range_eq_map, ← MonoidHom.range_eq_map, range_subtype, range_subtype]
    | succ n ih => rw [derivedSeries_succ, map_commutator, ih, derivedSeries_succ, map_commutator]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
n : ℕ
ih : Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)
⊢ Eq (α := Subgroup G) (derivedSeries G (n + 1).succ) (_root_.commutator G)
have succ : Eq.{u_1 + 1} (α := Subgroup G)
  (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
  (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
Tactic: rw [_root_.derivedSeries_succ, ih, _root_.commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
n : ℕ
ih : Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)
⊢ Eq.{u_1 + 1} (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
    (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
have succ : ∀ (h : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊥),
  Eq.{u_1 + 1} (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
    (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
Tactic: rcases (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
n : ℕ
ih : Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)
succ :
  ∀ (h : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊥),
    Eq.{u_1 + 1} (α := Subgroup G)
      (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
        (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
      (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
⊢ Eq.{u_1 + 1} (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
    (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
have succ₁ : ∀ (h : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤),
  Eq.{u_1 + 1} (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
    (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
Tactic: rcases (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
n : ℕ
ih : Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)
h : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
    (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
have succ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊥ ⊥) ⊥
Tactic: rw [h, commutator_bot_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
n : ℕ
ih : Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)
h : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊥
succ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊥ ⊥) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (Bracket.bracket (L := Subgroup G) ⊤ ⊤))
    (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
have succ₁ : Eq.{u_1 + 1} (α := Subgroup G) ⊥ ⊥
Tactic: rw [h, commutator_bot_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
n : ℕ
⊢ Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)
have zero : Eq (α := Subgroup G) (derivedSeries G (Nat.succ 0)) (_root_.commutator G)
Tactic: induction n with
  | zero => exact derivedSeries_one G
  | succ n ih =>
    rw [_root_.derivedSeries_succ, ih, _root_.commutator]
    rcases (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h | h
    · rw [h, commutator_bot_left]
    · rwa [h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
n : ℕ
zero : Eq (α := Subgroup G) (derivedSeries G (Nat.succ 0)) (_root_.commutator G)
⊢ Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)
have succ : ∀ (n : ℕ) (ih : Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)),
  Eq (α := Subgroup G) (derivedSeries G (n + 1).succ) (_root_.commutator G)
Tactic: induction n with
  | zero => exact derivedSeries_one G
  | succ n ih =>
    rw [_root_.derivedSeries_succ, ih, _root_.commutator]
    rcases (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h | h
    · rw [h, commutator_bot_left]
    · rwa [h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
n : ℕ
hn : Eq (α := Subgroup G) (derivedSeries G n) ⊥
⊢ ∀ (a b : G), a * b = b * a
have zero : ∀ (hn : Eq (α := Subgroup G) (derivedSeries G 0) ⊥) (a b : G), a * b = b * a
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
n : ℕ
hn : Eq (α := Subgroup G) (derivedSeries G n) ⊥
zero : ∀ (hn : Eq (α := Subgroup G) (derivedSeries G 0) ⊥) (a b : G), a * b = b * a
⊢ ∀ (a b : G), a * b = b * a
have succ : ∀ (n : ℕ) (hn : Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊥) (a b : G), a * b = b * a
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
hn : Eq (α := Subgroup G) (derivedSeries G 0) ⊥
a b : G
⊢ a * b = b * a
have zero : Membership.mem (γ := Subgroup G) ⊥ (a * b)
Tactic: refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
hn : Eq (α := Subgroup G) (derivedSeries G 0) ⊥
a b : G
zero : Membership.mem (γ := Subgroup G) ⊥ (a * b)
⊢ a * b = b * a
have zero₁ : Membership.mem (γ := Subgroup G) ⊥ (b * a)
Tactic: refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
hn : Eq (α := Subgroup G) (derivedSeries G 0) ⊥
a b : G
⊢ Membership.mem (γ := Subgroup G) ⊥ (a * b)
have zero : Membership.mem (γ := Subgroup G) (derivedSeries G 0) (a * b)
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
hn : Eq (α := Subgroup G) (derivedSeries G 0) ⊥
a b : G
⊢ Membership.mem (γ := Subgroup G) ⊥ (b * a)
have zero : Membership.mem (γ := Subgroup G) (derivedSeries G 0) (b * a)
Tactic: rw [← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
n : ℕ
hn : Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊥
⊢ ∀ (a b : G), a * b = b * a
have hn₁ : Eq (α := Subgroup G) (_root_.commutator G) ⊥
Tactic: rw [IsSimpleGroup.derivedSeries_succ] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
n : ℕ
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊥
a b : G
⊢ a * b = b * a
have succ : Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) (a * b * a⁻¹ * b⁻¹)
Tactic: rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (hypothesis)
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
⊢ ¬IsSolvable (Perm (Fin 5))
have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
Tactic: have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ ¬IsSolvable (Perm (Fin 5))
have refine : ∀ (n : ℕ), Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
Tactic: refine not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) x
have succ : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) ⁅x, y * x * y⁻¹⁆
Tactic: rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
have zero : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) 0) x
Tactic: induction n with
  | zero => exact mem_top x
  | succ n ih =>
    rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
    exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
y : Perm (Fin 5) := { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ }
z : Perm (Fin 5) := { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
zero : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) 0) x
⊢ Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x
have succ : ∀ (n : ℕ) (ih : Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) n) x),
  Membership.mem (γ := Subgroup (Perm (Fin 5))) (derivedSeries (Perm (Fin 5)) (n + 1)) x
Tactic: induction n with
  | zero => exact mem_top x
  | succ n ih =>
    rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
    exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)
Cleared hypotheses: n