awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
x y : N₁ ⋊[φ₁] G₁
h :
  Eq.{u_6 + 1} (α := N₂) ((MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) x.right) fn : (a : N₁) → N₂) y.left : N₂)
    ((fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) x.right)) : (a : N₁) → N₂) y.left : N₂)
left :
  SemidirectProduct.left.{u_6, u_7} (G := G₂) (φ := φ₂)
      ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    (HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)).left
right :
  SemidirectProduct.right.{u_6, u_7} (N := N₂) (φ := φ₂)
      ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    (HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)).right
⊢ ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
x y : N₁ ⋊[φ₁] G₁
h :
  Eq.{u_6 + 1} (α := N₂) ((MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) x.right) fn : (a : N₁) → N₂) y.left : N₂)
    ((fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) x.right)) : (a : N₁) → N₂) y.left : N₂)
⊢ left.{u_6, u_7} (G := G₂) (φ := φ₂) ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    (HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)).left

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
x y : N₁ ⋊[φ₁] G₁
h :
  Eq.{u_6 + 1} (α := N₂) ((MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) x.right) fn : (a : N₁) → N₂) y.left : N₂)
    ((fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) x.right)) : (a : N₁) → N₂) y.left : N₂)
⊢ right.{u_6, u_7} (N := N₂) (φ := φ₂) ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    (HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)).right

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
h :
  ∀ (g : G₁),
    MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) g) fn = fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))
x : G₁
h₁ :
  ∀ (x_1 : N₁),
    Eq.{u_6 + 1} (α := N₂) ((MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) x) fn : (a : N₁) → N₂) x_1 : N₂)
      ((fn.trans
              (((MonoidHom.comp (↑(MulAut.congr fn) : MulAut N₁ →* MulAut N₂) (φ₁.comp (↑fg.symm : G₂ →* G₁)) :
                    MonoidHom.{u_7, u_6} G₂ (MulAut N₂)) :
                  (a : G₂) → MulAut N₂)
                ((fg : (a : G₁) → G₂) x)) :
            (a : N₁) → N₂)
          x_1 :
        N₂)
⊢ MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) x) fn =
    fn.trans
      (((MonoidHom.comp (↑(MulAut.congr fn) : MulAut N₁ →* MulAut N₂) (φ₁.comp (↑fg.symm : G₂ →* G₁)) :
            MonoidHom.{u_7, u_6} G₂ (MulAut N₂)) :
          (a : G₂) → MulAut N₂)
        ((fg : (a : G₁) → G₂) x))

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ ≃* N₂
fg : G₁ ≃* G₂
h :
  ∀ (g : G₁),
    MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) g) fn = fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))
x : G₁
x_1 : N₁
⊢ Eq.{u_6 + 1} (α := N₂) ((MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) x) fn : (a : N₁) → N₂) x_1 : N₂)
    ((fn.trans
            (((MonoidHom.comp (↑(MulAut.congr fn) : MulAut N₁ →* MulAut N₂) (φ₁.comp (↑fg.symm : G₂ →* G₁)) :
                  MonoidHom.{u_7, u_6} G₂ (MulAut N₂)) :
                (a : G₂) → MulAut N₂)
              ((fg : (a : G₁) → G₂) x)) :
          (a : N₁) → N₂)
        x_1 :
      N₂)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
⊢ Nat.card (N ⋊[φ] G) = Nat.card N * Nat.card G

Tactic:
Nat.card_prod _ _ ▸ Nat.card_congr equivProd

Premises used: Eq.rec, Nat.card_congr, SemidirectProduct.equivProd, Nat.card_prod
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (derivedSeries G 0) ⊤

Tactic:
rfl

Premises used: derivedSeries, rfl
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
n : ℕ
⊢ Eq (α := Subgroup G) (derivedSeries G (n + 1))
    (Bracket.bracket (L := Subgroup G) (derivedSeries G n) (derivedSeries G n))

Tactic:
rfl

Premises used: derivedSeries, rfl
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
⊢ Normal (derivedSeries G 0)

Tactic:
(⊤ : Subgroup G).normal_of_characteristic

Premises used: Subgroup.normal_of_characteristic, derivedSeries, Top.top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
⊢ Normal (derivedSeries G 0)

Tactic:
exact (⊤ : Subgroup G).normal_of_characteristic

Premises used: Subgroup.normal_of_characteristic, Top.top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih : Normal (derivedSeries G n)
⊢ Normal (derivedSeries G (n + 1))

Tactic:
Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

Premises used: derivedSeries, Subgroup.commutator_normal
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
n : ℕ
ih : Normal (derivedSeries G n)
⊢ Normal (derivedSeries G (n + 1))

Tactic:
exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

Premises used: derivedSeries, Subgroup.commutator_normal
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
n : ℕ
zero : Normal (derivedSeries G 0)
succ : ∀ (n : ℕ) (ih : Normal (derivedSeries G n)), Normal (derivedSeries G (n + 1))
⊢ Normal (derivedSeries G n)

Tactic:
induction n with
  | zero => exact (⊤ : Subgroup G).normal_of_characteristic
  | succ n ih => exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

Premises used: Subgroup.normal_of_characteristic, Top.top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (derivedSeries G 1) (_root_.commutator G)

Tactic:
rfl

Premises used: Set.Mem, setOf, commutator, rfl
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
⊢ Antitone (β := Subgroup G) (derivedSeries G)

Tactic:
antitone_nat_of_succ_le fun n => (derivedSeries G n).commutator_le_self

Premises used: Subgroup.commutator_le_self, derivedSeries, antitone_nat_of_succ_le
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ Characteristic (derivedSeries G 0)

Tactic:
Subgroup.topCharacteristic

Premises used: derivedSeries, Subgroup.topCharacteristic
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ Characteristic (derivedSeries G 0)

Tactic:
exact Subgroup.topCharacteristic

Premises used: Subgroup.topCharacteristic
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
n : ℕ
h : Characteristic (derivedSeries G n)
⊢ Characteristic (derivedSeries G (n + 1))

Tactic:
Subgroup.commutator_characteristic _ _

Premises used: derivedSeries, Subgroup.commutator_characteristic
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
n : ℕ
h : Characteristic (derivedSeries G n)
⊢ Characteristic (derivedSeries G (n + 1))

Tactic:
exact Subgroup.commutator_characteristic _ _

Premises used: Subgroup.commutator_characteristic
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
n : ℕ
zero : Characteristic (derivedSeries G 0)
succ : ∀ (n : ℕ), Characteristic (derivedSeries G n) → Characteristic (derivedSeries G (n + 1))
⊢ Characteristic (derivedSeries G n)

Tactic:
induction n with
  | zero => exact Subgroup.topCharacteristic
  | succ n _ => exact Subgroup.commutator_characteristic _ _

Premises used: Subgroup.topCharacteristic, Subgroup.commutator_characteristic
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ map f (derivedSeries G 0) ≤ derivedSeries G' 0

Tactic:
le_top

Premises used: Set.Mem, le_top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
⊢ map f (derivedSeries G 0) ≤ derivedSeries G' 0

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
n : ℕ
ih : map f (derivedSeries G n) ≤ derivedSeries G' n
⊢ map f (derivedSeries G (n + 1)) ≤ derivedSeries G' (n + 1)

Tactic:
simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]

Premises used: Subgroup.commutator_mono, derivedSeries_succ, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
n : ℕ
zero : map f (derivedSeries G 0) ≤ derivedSeries G' 0
succ :
  ∀ (n : ℕ) (ih : map f (derivedSeries G n) ≤ derivedSeries G' n),
    map f (derivedSeries G (n + 1)) ≤ derivedSeries G' (n + 1)
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n

Tactic:
induction n with
  | zero => exact le_top
  | succ n ih => simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]

Premises used: Subgroup.commutator_mono, derivedSeries_succ, le_top, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ derivedSeries G' 0 ≤ map f (derivedSeries G 0)

Tactic:
(map_top_of_surjective f hf).ge

Premises used: Eq.ge, Set.Mem, Subgroup.map_top_of_surjective
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ derivedSeries G' 0 ≤ map f (derivedSeries G 0)

Tactic:
exact (map_top_of_surjective f hf).ge

Premises used: Eq.ge, Subgroup.map_top_of_surjective
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
ih : derivedSeries G' n ≤ map f (derivedSeries G n)
⊢ derivedSeries G' (n + 1) ≤ map f (derivedSeries G (n + 1))

Tactic:
commutator_le_map_commutator ih ih

Premises used: Set.Mem, Subgroup.commutator_le_map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
ih : derivedSeries G' n ≤ map f (derivedSeries G n)
⊢ derivedSeries G' (n + 1) ≤ map f (derivedSeries G (n + 1))

Tactic:
exact commutator_le_map_commutator ih ih

Premises used: Subgroup.commutator_le_map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
zero : derivedSeries G' 0 ≤ map f (derivedSeries G 0)
succ :
  ∀ (n : ℕ) (ih : derivedSeries G' n ≤ map f (derivedSeries G n)),
    derivedSeries G' (n + 1) ≤ map f (derivedSeries G (n + 1))
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)

Tactic:
induction n with
  | zero => exact (map_top_of_surjective f hf).ge
  | succ n ih => exact commutator_le_map_commutator ih ih

Premises used: Eq.ge, Subgroup.map_top_of_surjective
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
n : ℕ
⊢ map f (derivedSeries G n) = derivedSeries G' n

Tactic:
le_antisymm (map_derivedSeries_le_derivedSeries f n) (derivedSeries_le_map_derivedSeries hf n)

Premises used: derivedSeries_le_map_derivedSeries, map_derivedSeries_le_derivedSeries, le_antisymm
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G_1 : Type u_1
G' : Type u_2
inst : Group G_1
inst_1 : Group G'
f : G_1 →* G'
G : Type u_3
inst_2 : CommGroup G
⊢ IsSolvable G

Tactic:
⟨⟨1, le_bot_iff.mp (Abelianization.commutator_subset_ker (MonoidHom.id G))⟩⟩

Premises used: le_bot_iff, MonoidHom.id, Exists.intro, Iff.mp, OfNat.ofNat, IsSolvable.mk, Abelianization.commutator_subset_ker
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := { toGroup := hG, mul_comm := h }
mk :
  ∀ [toDivInvMonoid : DivInvMonoid G] (inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1) (h : ∀ (a b : G), a * b = b * a),
    IsSolvable G
⊢ IsSolvable G

Tactic:
cases hG
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_3
toDivInvMonoid : DivInvMonoid G
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := { toDivInvMonoid := toDivInvMonoid, inv_mul_cancel := inv_mul_cancel, mul_comm := h }
⊢ IsSolvable G

Tactic:
CommGroup.isSolvable

Premises used: CommGroup.isSolvable
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_3
toDivInvMonoid : DivInvMonoid G
inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := { toDivInvMonoid := toDivInvMonoid, inv_mul_cancel := inv_mul_cancel, mul_comm := h }
⊢ IsSolvable G

Tactic:
exact CommGroup.isSolvable

Premises used: CommGroup.isSolvable
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
h : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊥
⊢ IsSolvable G

Tactic:
⟨⟨0, h⟩⟩

Premises used: Exists.intro, OfNat.ofNat, IsSolvable.mk
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : Subsingleton G
⊢ Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊥

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
obtain : ∀ (n : ℕ) (hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥), IsSolvable G
⊢ IsSolvable G

Tactic:
obtain ⟨n, hn⟩ := id hG''

Premises used: id
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
obtain : ∀ (m : ℕ) (hm : Eq (α := Subgroup G') (derivedSeries G' m) ⊥), IsSolvable G
⊢ IsSolvable G

Tactic:
obtain ⟨m, hm⟩ := id hG'

Premises used: id
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
m : ℕ
hm : Eq (α := Subgroup G') (derivedSeries G' m) ⊥
⊢ IsSolvable G

Tactic:
⟨⟨n + m, le_bot_iff.mp (Subgroup.map_bot f ▸ hm ▸ ?_)⟩⟩

Premises used: le_bot_iff, Eq.rec, Subgroup.map_bot, HAdd.hAdd, Exists.intro, Iff.mp, IsSolvable.mk
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
m : ℕ
hm : Eq (α := Subgroup G') (derivedSeries G' m) ⊥
refine : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ IsSolvable G

Tactic:
refine ⟨⟨n + m, le_bot_iff.mp (Subgroup.map_bot f ▸ hm ▸ ?_)⟩⟩
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
⊢ derivedSeries G (n + 0) ≤ map f (derivedSeries G' 0)

Tactic:
f.range_eq_map ▸ ((derivedSeries G n).map_eq_bot_iff.mp
      (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg

Premises used: le_bot_iff, Set.Mem, MonoidHom.range_eq_map, map_derivedSeries_le_derivedSeries, Eq.rec, Eq.le, Subgroup.map_eq_bot_iff, derivedSeries, Iff.mp, LE.le.trans
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
⊢ derivedSeries G (n + 0) ≤ map f (derivedSeries G' 0)

Tactic:
exact f.range_eq_map ▸ ((derivedSeries G n).map_eq_bot_iff.mp
      (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
m : ℕ
hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ derivedSeries G (n + (m + 1)) ≤ map f (derivedSeries G' (m + 1))

Tactic:
commutator_le_map_commutator hm hm

Premises used: Set.Mem, Subgroup.commutator_le_map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
m : ℕ
hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ derivedSeries G (n + (m + 1)) ≤ map f (derivedSeries G' (m + 1))

Tactic:
exact commutator_le_map_commutator hm hm

Premises used: Subgroup.commutator_le_map_commutator
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
G' : Type u_3
G'' : Type u_4
inst_1 : Group G'
inst_2 : Group G''
f : G' →* G
g : G →* G''
hfg : g.ker ≤ f.range
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥
m : ℕ
zero : derivedSeries G (n + 0) ≤ map f (derivedSeries G' 0)
succ :
  ∀ (m : ℕ) (hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)),
    derivedSeries G (n + (m + 1)) ≤ map f (derivedSeries G' (m + 1))
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)

Tactic:
induction m with
  | zero =>
    exact f.range_eq_map ▸ ((derivedSeries G n).map_eq_bot_iff.mp
      (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg
  | succ m hm => exact commutator_le_map_commutator hm hm
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
inst_2 : IsSolvable G'
⊢ IsSolvable G

Tactic:
solvable_of_ker_le_range (1 : G' →* G) f ((f.ker_eq_bot_iff.mpr hf).symm ▸ bot_le)

Premises used: solvable_of_ker_le_range, Iff.mpr, Eq.rec, MonoidHom.ker_eq_bot_iff, OfNat.ofNat, Eq.symm, bot_le
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
H : Subgroup G
inst_2 : IsSolvable G
⊢ IsSolvable.{u_1} ↥H

Tactic:
solvable_of_solvable_injective H.subtype_injective

Premises used: Subgroup.subtype_injective, solvable_of_solvable_injective
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
inst_2 : IsSolvable G
⊢ IsSolvable G'

Tactic:
solvable_of_ker_le_range f (1 : G' →* G) (f.range_eq_top_of_surjective hf ▸ le_top)

Premises used: solvable_of_ker_le_range, Eq.rec, MonoidHom.range_eq_top_of_surjective, le_top, OfNat.ofNat, Eq.symm
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
H : Subgroup G
inst_2 : H.Normal
inst_3 : IsSolvable G
⊢ IsSolvable.{u_1} (G ⧸ H)

Tactic:
solvable_of_surjective (QuotientGroup.mk'_surjective H)

Premises used: solvable_of_surjective, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
G'_1 : Type u_2
inst : Group G
inst_1 : Group G'_1
f : G →* G'_1
G' : Type u_3
inst_2 : Group G'
inst_3 : IsSolvable G
inst_4 : IsSolvable G'
⊢ IsSolvable (G × G')

Tactic:
solvable_of_ker_le_range (MonoidHom.inl G G') (MonoidHom.snd G G') fun x hx =>
    ⟨x.1, Prod.ext rfl hx.symm⟩

Premises used: solvable_of_ker_le_range, MonoidHom.inl, Prod.fst, Prod.ext, Exists.intro, Eq.symm, rfl, MonoidHom.snd
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
hG : IsSolvable G
inst_1 : Nontrivial G
rw : Ne (α := Subgroup G) (_root_.commutator G) ⊤
⊢ LT.lt (α := Subgroup G) (_root_.commutator G) ⊤

Tactic:
rw [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
hG : IsSolvable G
inst_1 : Nontrivial G
obtain : ∀ (n : ℕ) (hn : Eq (α := Subgroup G) (derivedSeries G n) ⊥), Ne (α := Subgroup G) (_root_.commutator G) ⊤
⊢ Ne (α := Subgroup G) (_root_.commutator G) ⊤

Tactic:
obtain ⟨n, hn⟩ := hG
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
n : ℕ
hn : Eq (α := Subgroup G) (derivedSeries G n) ⊥
contrapose! : ∀ (hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤), Ne (α := Subgroup G) (derivedSeries G n) ⊥
⊢ Ne (α := Subgroup G) (_root_.commutator G) ⊤

Tactic:
contrapose! hn
-- Module: Mathlib.GroupTheory.Solvable
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
n : ℕ
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ Ne (α := Subgroup G) (derivedSeries G n) ⊥

Tactic:
ne_of_eq_of_ne ?_ top_ne_bot

Premises used: ne_of_eq_of_ne, top_ne_bot