awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst : Group N₁
inst_1 : Group G₁
inst_2 : Group N₂
inst_3 : 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₁),
    fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))) fn
⊢ (map fn fg h).comp inr = MonoidHom.comp inr fg
have h₁ : ∀ (x : G₁),
  Eq.{u_6 + 1} (α := N₂) (left.{u_6, u_7} (G := G₂) (φ := φ₂) (((map fn fg h).comp inr : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
    (left.{u_6, u_7} (G := G₂) (φ := φ₂) ((MonoidHom.comp inr fg : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst : Group N₁
inst_1 : Group G₁
inst_2 : Group N₂
inst_3 : 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₁),
    fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))) fn
h₁ :
  ∀ (x : G₁),
    Eq.{u_6 + 1} (α := N₂) (left.{u_6, u_7} (G := G₂) (φ := φ₂) (((map fn fg h).comp inr : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
      (left.{u_6, u_7} (G := G₂) (φ := φ₂) ((MonoidHom.comp inr fg : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
⊢ (map fn fg h).comp inr = MonoidHom.comp inr fg
have h₂ : ∀ (x : G₁),
  Eq.{u_7 + 1} (α := G₂) (right.{u_6, u_7} (N := N₂) (φ := φ₂) (((map fn fg h).comp inr : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
    (right.{u_6, u_7} (N := N₂) (φ := φ₂) ((MonoidHom.comp inr fg : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (hypothesis)
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 y : N₁ ⋊[φ₁] 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₂)
have 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₂)
Tactic: replace h := DFunLike.ext_iff.1 (h x.right) y.left
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
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₂)
⊢ ⟨(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₂)
have left : 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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
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
⊢ ⟨(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₂)
have right : 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: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
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₁
⊢ 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))
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
⊢ Normal (derivedSeries G n)
have zero : Normal (derivedSeries G 0)
Tactic: induction n with
  | zero => exact (⊤ : Subgroup G).normal_of_characteristic
  | succ n ih => exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
n : ℕ
zero : Normal (derivedSeries G 0)
⊢ Normal (derivedSeries G n)
have succ : ∀ (n : ℕ) (ih : Normal (derivedSeries G n)), Normal (derivedSeries G (n + 1))
Tactic: induction n with
  | zero => exact (⊤ : Subgroup G).normal_of_characteristic
  | succ n ih => exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
n : ℕ
⊢ Characteristic (derivedSeries G n)
have zero : Characteristic (derivedSeries G 0)
Tactic: induction n with
  | zero => exact Subgroup.topCharacteristic
  | succ n _ => exact Subgroup.commutator_characteristic _ _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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)
⊢ Characteristic (derivedSeries G n)
have succ : ∀ (n : ℕ), Characteristic (derivedSeries G n) → Characteristic (derivedSeries G (n + 1))
Tactic: induction n with
  | zero => exact Subgroup.topCharacteristic
  | succ n _ => exact Subgroup.commutator_characteristic _ _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
n : ℕ
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n
have zero : map f (derivedSeries G 0) ≤ derivedSeries G' 0
Tactic: induction n with
  | zero => exact le_top
  | succ n ih => simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n
have succ : ∀ (n : ℕ) (ih : map f (derivedSeries G n) ≤ derivedSeries G' n),
  map f (derivedSeries G (n + 1)) ≤ derivedSeries G' (n + 1)
Tactic: induction n with
  | zero => exact le_top
  | succ n ih => simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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 : ℕ
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)
have zero : derivedSeries G' 0 ≤ map f (derivedSeries G 0)
Tactic: induction n with
  | zero => exact (map_top_of_surjective f hf).ge
  | succ n ih => exact commutator_le_map_commutator ih ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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)
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)
have succ : ∀ (n : ℕ) (ih : derivedSeries G' n ≤ map f (derivedSeries G n)),
  derivedSeries G' (n + 1) ≤ map f (derivedSeries G (n + 1))
Tactic: induction n with
  | zero => exact (map_top_of_surjective f hf).ge
  | succ n ih => exact commutator_le_map_commutator ih ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := { toGroup := hG, mul_comm := h }
⊢ IsSolvable G
have mk : ∀ [toDivInvMonoid : DivInvMonoid G] (inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1) (h : ∀ (a b : G), a * b = b * a),
  IsSolvable G
Tactic: cases hG
Cleared hypotheses: hG, h, hG'
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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''
⊢ IsSolvable G
have obtain : ∀ (n : ℕ) (hn : Eq (α := Subgroup G'') (derivedSeries G'' n) ⊥), IsSolvable G
Tactic: obtain ⟨n, hn⟩ := id hG''
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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) ⊥
⊢ IsSolvable G
have obtain : ∀ (m : ℕ) (hm : Eq (α := Subgroup G') (derivedSeries G' m) ⊥), IsSolvable G
Tactic: obtain ⟨m, hm⟩ := id hG'
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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
have refine : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
Tactic: refine ⟨⟨n + m, le_bot_iff.mp (Subgroup.map_bot f ▸ hm ▸ ?_)⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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 : ℕ
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
have zero : derivedSeries G (n + 0) ≤ map f (derivedSeries G' 0)
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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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)
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
have succ : ∀ (m : ℕ) (hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)),
  derivedSeries G (n + (m + 1)) ≤ map f (derivedSeries G' (m + 1))
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
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
hG : IsSolvable G
inst_1 : Nontrivial G
⊢ LT.lt (α := Subgroup G) (_root_.commutator G) ⊤
have rw : Ne (α := Subgroup G) (_root_.commutator G) ⊤
Tactic: rw [lt_top_iff_ne_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
hG : IsSolvable G
inst_1 : Nontrivial G
⊢ Ne (α := Subgroup G) (_root_.commutator G) ⊤
have obtain : ∀ (n : ℕ) (hn : Eq (α := Subgroup G) (derivedSeries G n) ⊥), Ne (α := Subgroup G) (_root_.commutator G) ⊤
Tactic: obtain ⟨n, hn⟩ := hG
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
n : ℕ
hn : Eq (α := Subgroup G) (derivedSeries G n) ⊥
⊢ Ne (α := Subgroup G) (_root_.commutator G) ⊤
have contrapose! : ∀ (hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤), Ne (α := Subgroup G) (derivedSeries G n) ⊥
Tactic: contrapose! hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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) ⊥
have refine : Eq (α := Subgroup G) (derivedSeries G n) ⊤
Tactic: refine ne_of_eq_of_ne ?_ top_ne_bot
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊤
have succ : Eq (α := Subgroup G) (Bracket.bracket (L := Subgroup G) (derivedSeries G n) (derivedSeries G n)) ⊤
Tactic: rwa [derivedSeries_succ, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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)) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊤
have succ₁ : Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤
Tactic: rwa [derivedSeries_succ, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
n : ℕ
hn : Eq (α := Subgroup G) (_root_.commutator G) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G n) ⊤
have zero : Eq (α := Subgroup G) (derivedSeries G 0) ⊤
Tactic: induction n with
  | zero => exact derivedSeries_zero G
  | succ n h => rwa [derivedSeries_succ, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
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) ⊤
⊢ Eq (α := Subgroup G) (derivedSeries G n) ⊤
have succ : ∀ (n : ℕ) (h : Eq (α := Subgroup G) (derivedSeries G n) ⊤), Eq (α := Subgroup G) (derivedSeries G (n + 1)) ⊤
Tactic: induction n with
  | zero => exact derivedSeries_zero G
  | succ n h => rwa [derivedSeries_succ, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSolvable G
H : Subgroup G
hH : H ≠ ⊥
⊢ ⁅H, H⁆ < H
have hH₁ : Nontrivial.{u_1} ↥H
Tactic: rw [← nontrivial_iff_ne_bot] at hH
Cleared hypotheses: hH
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : IsSolvable G
H : Subgroup G
hH : Nontrivial.{u_1} ↥H
⊢ ⁅H, H⁆ < H
have rw : LT.lt.{u_1} (α := Subgroup ↥H) (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) ⊤
Tactic: rw [← H.range_subtype, MonoidHom.range_eq_map, ← map_commutator, map_subtype_lt_map_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)
⊢ IsSolvable G ↔ ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
have refine : ∀ (h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H), IsSolvable G
Tactic: refine ⟨fun _ _ ↦ IsSolvable.commutator_lt_of_ne_bot, fun h ↦ ?_⟩
-- 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
⊢ IsSolvable G
have suffices : IsSolvable.{u_1} ↥⊤
Tactic: suffices h : IsSolvable (⊤ : Subgroup G) from
    solvable_of_surjective (MonoidHom.range_eq_top.mp (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
⊢ IsSolvable.{u_1} ↥⊤
have ind : ∀ (H : Subgroup G) (hH : ∀ y < H, IsSolvable.{u_1} ↥y), IsSolvable.{u_1} ↥H
Tactic: induction (⊤ : Subgroup G) using WellFoundedLT.induction with | ind H hH
-- 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
⊢ IsSolvable.{u_1} ↥H
have ind : ∀ (hH : ∀ y < ⊥, IsSolvable.{u_1} ↥y), IsSolvable.{u_1} ↥⊥
Tactic: rcases eq_or_ne H ⊥ with rfl | h'
Cleared hypotheses: H, hH
-- 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
ind : ∀ (hH : ∀ y < ⊥, IsSolvable.{u_1} ↥y), IsSolvable.{u_1} ↥⊥
⊢ IsSolvable.{u_1} ↥H
have ind₁ : ∀ (h' : H ≠ ⊥), IsSolvable.{u_1} ↥H
Tactic: rcases eq_or_ne H ⊥ with rfl | h'
-- 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 ≠ ⊥
⊢ IsSolvable.{u_1} ↥H
have ind : ∀ (n : ℕ) (hn : Eq.{u_1 + 1} (α := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) ⊥), IsSolvable.{u_1} ↥H
Tactic: obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')
-- 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 : ℕ
hn : Eq.{u_1 + 1} (α := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) ⊥
⊢ IsSolvable.{u_1} ↥H
have h₁ : Eq.{u_1 + 1} (α := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) ⊥
Tactic: use n + 1
-- 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 : ℕ
hn : Eq.{u_1 + 1} (α := Subgroup ↥⁅H, H⁆) (derivedSeries (↥⁅H, H⁆) n) ⊥
⊢ Eq.{u_1 + 1} (α := Subgroup ↥H) (derivedSeries (↥H) (n + 1)) ⊥
have h₁ : ∀ (hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥), map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥
Tactic: rw [← map_subtype_inj, Subgroup.map_bot] at hn ⊢
Cleared hypotheses: hn
-- 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 : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥
have h₁ : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
Tactic: rw [← hn]
-- 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 ≠ ⊥
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₁ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) (derivedSeries (↥H) 0) (derivedSeries (↥H) 0)) =
  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]
-- 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)
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₂ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = 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]
-- 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)
⊢ map H.subtype (derivedSeries (↥H) (HAdd.hAdd (α := ℕ) 0 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) 0)
have h₃ : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = 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]