awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
n : ℕ
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤
refine : Eq (α := Subgroup G) (derivedSeries G n) ⊤
⊢ Ne (α := Subgroup G) (derivedSeries G n) ⊥

Tactic:
refine ne_of_eq_of_ne ?_ top_ne_bot

Premises used: ne_of_eq_of_ne, top_ne_bot
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G 0) ⊤

Tactic:
derivedSeries_zero G

Premises used: derivedSeries_zero
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G 0) ⊤

Tactic:
exact derivedSeries_zero G

Premises used: derivedSeries_zero
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤
n : ℕ
h : Eq (α := Subgroup G) (derivedSeries G n) ⊤
succ : Eq (α := Subgroup G) (Bracket.bracket (L := Subgroup G) (derivedSeries G n) (derivedSeries G n)) ⊤
succ₁ succ₂ succ₃ succ₄ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊤

Tactic:
rwa [derivedSeries_succ, h]

Premises used: derivedSeries_succ
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
n : ℕ
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤
zero : Eq (α := Subgroup G) (derivedSeries G 0) ⊤
succ : ∀ (n : ℕ) (h : Eq (α := Subgroup G) (derivedSeries G n) ⊤), Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G n) ⊤

Tactic:
induction n with
  | zero => exact derivedSeries_zero G
  | succ n h => rwa [derivedSeries_succ, h]

Premises used: derivedSeries_zero, derivedSeries_succ
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSolvable G
H : Subgroup G
hH : H ≠ ⊥
⊢ Nontrivial.{u_1} ↥H

Tactic:
rw [← nontrivial_iff_ne_bot] at hH

Premises used: Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSolvable G
H : Subgroup G
hH : Nontrivial.{u_1} ↥H
rw : LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤
⊢ ⁅H, H⁆ < H

Tactic:
rw [← H.range_subtype, MonoidHom.range_eq_map, ← map_commutator, map_subtype_lt_map_subtype]

Premises used: MonoidHom.range_eq_map, Subgroup.map_subtype_lt_map_subtype, Subgroup.range_subtype, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSolvable G
H : Subgroup G
hH : Nontrivial.{u_1} ↥H
⊢ LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤

Tactic:
commutator_lt_top_of_nontrivial H

Premises used: IsSolvable.commutator_lt_top_of_nontrivial, Membership.mem, Subtype
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSolvable G
H : Subgroup G
hH : Nontrivial.{u_1} ↥H
⊢ LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤

Tactic:
exact commutator_lt_top_of_nontrivial H

Premises used: IsSolvable.commutator_lt_top_of_nontrivial, Membership.mem, Subtype
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
⊢ IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H

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

Premises used: IsSolvable.commutator_lt_of_ne_bot, Iff.intro
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
refine : ∀ (h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H), IsSolvable G
⊢ IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H

Tactic:
refine ⟨fun _ _ ↦ IsSolvable.commutator_lt_of_ne_bot, fun h ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
suffices : IsSolvable.{u_1} ↥⊤
⊢ IsSolvable G

Tactic:
suffices h : IsSolvable (⊤ : Subgroup G) from
    solvable_of_surjective (MonoidHom.range_eq_top.mp (range_subtype ⊤))
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
ind : ∀ (H : Subgroup G) (hH : ∀ y < H, IsSolvable.{u_1} ↥y), IsSolvable.{u_1} ↥H
⊢ IsSolvable.{u_1} ↥⊤

Tactic:
induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH

Premises used: WellFoundedLT.induction, Top.top
-- Module: Mathlib.GroupTheory.Solvable
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
ind : ∀ (hH : ∀ y < ⊥, IsSolvable.{u_1} ↥y), IsSolvable.{u_1} ↥⊥
ind₁ : ∀ (h' : H ≠ ⊥), IsSolvable.{u_1} ↥H
⊢ IsSolvable.{u_1} ↥H

Tactic:
rcases eq_or_ne H ⊥ with rfl | h'

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : WellFoundedLT.{u_1} (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
hH : ∀ y < ⊥, IsSolvable.{u_1} ↥y
⊢ IsSolvable.{u_1} ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.Solvable
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 ≠ ⊥
ind : ∀ (n : ℕ) (hn : Eq.{u_1 + 1} (α := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) ⊥), IsSolvable.{u_1} ↥H
⊢ IsSolvable.{u_1} ↥H

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

Premises used: Bracket.bracket
-- Module: Mathlib.GroupTheory.Solvable
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 : ℕ
hn : Eq.{u_1 + 1} (α := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) ⊥
h₁ : Eq.{u_1 + 1} (α := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) ⊥
⊢ IsSolvable.{u_1} ↥H

Tactic:
use n + 1
-- Module: Mathlib.GroupTheory.Solvable
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 : ℕ
hn : Eq.{u_1 + 1} (α := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) ⊥
h₁ : ∀ (hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥), map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) ⊥

Tactic:
rw [← map_subtype_inj, Subgroup.map_bot] at hn ⊢

Premises used: Subgroup.map_subtype_inj, Subgroup.map_bot
-- Module: Mathlib.GroupTheory.Solvable
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 : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
h₁ : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥

Tactic:
rw [← hn]
-- Module: Mathlib.GroupTheory.Solvable
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
h₈ h₉ : ⁅H, H⁆ = ⁅H, H⁆
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 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]

Premises used: derivedSeries_zero, derivedSeries_succ, MonoidHom.range_eq_map, Subgroup.range_subtype, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Solvable
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))
h₅ 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)⁆
⊢ 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]

Premises used: derivedSeries_succ, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Solvable
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)
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))
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)

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]

Premises used: derivedSeries_zero, derivedSeries_succ, MonoidHom.range_eq_map, Subgroup.range_subtype, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
⊢ Eq (α := Subgroup G) (derivedSeries G (Nat.succ 0)) (_root_.commutator G)

Tactic:
derivedSeries_one G

Premises used: derivedSeries_one
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
⊢ Eq (α := Subgroup G) (derivedSeries G (Nat.succ 0)) (_root_.commutator G)

Tactic:
exact derivedSeries_one G

Premises used: derivedSeries_one
-- Module: Mathlib.GroupTheory.Solvable
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 :
  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 (α := Subgroup G) (derivedSeries G (n + 1).succ) (_root_.commutator G)

Tactic:
rw [_root_.derivedSeries_succ, ih, _root_.commutator]

Premises used: derivedSeries_succ, commutator
-- Module: Mathlib.GroupTheory.Solvable
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) ⊤ ⊤)
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) ⊤ ⊤)

Tactic:
rcases (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h | h

Premises used: Top.top, Subgroup.Normal.eq_bot_or_eq_top, Subgroup.commutator_normal
-- Module: Mathlib.GroupTheory.Solvable
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) ⊥ ⊥) ⊥
succ₁ succ₂ : Eq.{u_1 + 1} (α := 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:
rw [h, commutator_bot_left]

Premises used: Subgroup.commutator_bot_left
-- Module: Mathlib.GroupTheory.Solvable
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 succ succ₁ succ₂ 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) ⊤ ⊤)

Tactic:
rwa [h]
-- Module: Mathlib.GroupTheory.Solvable
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)
succ :
  ∀ (n : ℕ) (ih : Eq (α := Subgroup G) (derivedSeries G n.succ) (_root_.commutator G)),
    Eq (α := Subgroup G) (derivedSeries G (n + 1).succ) (_root_.commutator G)
⊢ Eq (α := Subgroup G) (derivedSeries G n.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]

Premises used: derivedSeries_succ, commutator, derivedSeries_one, Top.top, Subgroup.Normal.eq_bot_or_eq_top, Subgroup.commutator_bot_left, Subgroup.commutator_normal
-- Module: Mathlib.GroupTheory.Solvable
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
succ : ∀ (n : ℕ) (hn : Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊥) (a b : G), a * b = b * a
⊢ ∀ (a b : G), a * b = b * a

Tactic:
cases n
-- Module: Mathlib.GroupTheory.Solvable
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

Tactic:
(mem_bot.1 ?_).trans (mem_bot.1 ?_).symm

Premises used: Iff.mp, Eq.symm, Subgroup.mem_bot, Eq.trans
-- Module: Mathlib.GroupTheory.Solvable
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)
zero₁ : Membership.mem (γ := Subgroup G) ⊥ (b * a)
⊢ a * b = b * a

Tactic:
refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm

Premises used: Iff.mp, Eq.symm, Subgroup.mem_bot, Eq.trans
-- Module: Mathlib.GroupTheory.Solvable
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) (derivedSeries G 0) (a * b)
⊢ Membership.mem (γ := Subgroup G) ⊥ (a * b)

Tactic:
rw [← hn]
-- Module: Mathlib.GroupTheory.Solvable
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) (derivedSeries G 0) (a * b)

Tactic:
mem_top _

Premises used: Set.Mem, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Solvable
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) (derivedSeries G 0) (a * b)

Tactic:
exact mem_top _

Premises used: Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Solvable
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) (derivedSeries G 0) (b * a)
⊢ Membership.mem (γ := Subgroup G) ⊥ (b * a)

Tactic:
rw [← hn]
-- Module: Mathlib.GroupTheory.Solvable
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) (derivedSeries G 0) (b * a)

Tactic:
mem_top _

Premises used: Set.Mem, Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Solvable
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) (derivedSeries G 0) (b * a)

Tactic:
exact mem_top _

Premises used: Subgroup.mem_top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSimpleGroup G
h : IsSolvable G
n : ℕ
hn : Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊥
⊢ Eq (α := Subgroup G) (_root_.commutator G) ⊥

Tactic:
rw [IsSimpleGroup.derivedSeries_succ] at hn

Premises used: IsSimpleGroup.derivedSeries_succ
-- Module: Mathlib.GroupTheory.Solvable
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
succ : Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) (a * b * a⁻¹ * b⁻¹)
⊢ a * b = b * a

Tactic:
rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]

Premises used: mul_inv_eq_one, mul_assoc, commutator_eq_closure, mul_inv_rev, Subgroup.mem_bot
-- Module: Mathlib.GroupTheory.Solvable
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
⊢ Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) (a * b * a⁻¹ * b⁻¹)

Tactic:
subset_closure ⟨a, b, rfl⟩

Premises used: Subgroup.subset_closure, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Solvable
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
⊢ Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) (a * b * a⁻¹ * b⁻¹)

Tactic:
exact subset_closure ⟨a, b, rfl⟩
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
g : G
h1 : g ≠ 1
h2 : ∀ (n : ℕ), Membership.mem (γ := Subgroup G) (derivedSeries G n) g
⊢ ¬IsSolvable G

Tactic:
mt (isSolvable_def _).mp
    (not_exists_of_forall_not fun n h =>
      h1 (Subgroup.mem_bot.mp ((congr_arg (g ∈ ·) h).mp (h2 n))))

Premises used: not_exists_of_forall_not, Membership.mem, mt, Eq.mp, congr_arg, isSolvable_def, Iff.mp, Subgroup.mem_bot
-- Module: Mathlib.GroupTheory.Solvable
Goal:
⊢ Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
Goal:
⊢ Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
⊢ Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
Goal:
x : Perm (Fin 5) := { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ }
⊢ Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
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 := ⋯ }
⊢ Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
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 := ⋯ }
⊢ Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
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 := ⋯ }
unfold :
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } =
    { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } *
        ⁅{ toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 },
          { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } *
              { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } *
            { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ :
                Fin 5 ≃ Fin 5 }⁻¹⁆ *
      { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 }⁻¹
⊢ x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹

Tactic:
unfold x y z
-- Module: Mathlib.GroupTheory.Solvable
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 := ⋯ }
⊢ { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } =
    { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } *
        ⁅{ toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 },
          { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } *
              { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 } *
            { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1], left_inv := ⋯, right_inv := ⋯ :
                Fin 5 ≃ Fin 5 }⁻¹⁆ *
      { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4], left_inv := ⋯, right_inv := ⋯ : Fin 5 ≃ Fin 5 }⁻¹

Tactic:
decide
-- Module: Mathlib.GroupTheory.Solvable
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 := ⋯ }
⊢ x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹

Tactic:
have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by unfold x y z; decide