awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : H.normalCore.relIndex H = 1
h : H = H.normalCore
⊢ H.Normal

Tactic:
convert! H.normalCore_normal

Premises used: Subgroup.normalCore_normal
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : H.normalCore.relIndex H = 1
⊢ H = H.normalCore

Tactic:
le_antisymm (relIndex_eq_one.mp this) (normalCore_le H)

Premises used: le_antisymm, Subgroup.relIndex_eq_one, Iff.mp, Subgroup.normalCore_le
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : H.normalCore.relIndex H = 1
⊢ H = H.normalCore

Tactic:
exact le_antisymm (relIndex_eq_one.mp this) (normalCore_le H)

Premises used: le_antisymm, Subgroup.relIndex_eq_one, Iff.mp, Subgroup.normalCore_le
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
neg : H.normalCore.relIndex H = 1
⊢ H.Normal

Tactic:
suffices H.normalCore.relIndex H = 1 by
    convert! H.normalCore_normal
    exact le_antisymm (relIndex_eq_one.mp this) (normalCore_le H)
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ Finite G

Tactic:
have : Finite G := finite_of_card_ne_zero hG0
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
⊢ H.index ≠ 0

Tactic:
have index_ne_zero : H.index ≠ 0 := index_ne_zero_of_finite
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
neg : H.normalCore.index = H.index
⊢ H.normalCore.relIndex H = 1

Tactic:
rw [← mul_left_inj' index_ne_zero, one_mul, relIndex_mul_index H.normalCore_le]

Premises used: Subgroup.relIndex_mul_index, mul_left_inj', Subgroup.normalCore_le, one_mul
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ Nat.Prime H.index

Tactic:
have hp : Nat.Prime H.index := hHp ▸ minFac_prime hG1
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
rw : Nat.card.{u_1} ↥(range (toPermHom G (G ⧸ H))) ∣ Nat.card.{u_1} (Equiv.Perm (G ⧸ H))
⊢ H.normalCore.index ∣ H.index !

Tactic:
rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]

Premises used: Nat.card_perm, Subgroup.index_ker, Subgroup.index_eq_card, Subgroup.normalCore_eq_ker
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card.{u_1} ↥(range (toPermHom G (G ⧸ H))) ∣ Nat.card.{u_1} (Equiv.Perm (G ⧸ H))

Tactic:
card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range

Premises used: MonoidHom.range, MulAction.toPermHom, HasQuotient.Quotient, Subgroup.card_subgroup_dvd_card
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card.{u_1} ↥(range (toPermHom G (G ⧸ H))) ∣ Nat.card.{u_1} (Equiv.Perm (G ⧸ H))

Tactic:
exact card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range

Premises used: MonoidHom.range, MulAction.toPermHom, HasQuotient.Quotient, Subgroup.card_subgroup_dvd_card
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ H.normalCore.index ∣ H.index !

Tactic:
have h : H.normalCore.index ∣ H.index ! := by
    rw [normalCore_eq_ker, index_ker, index_eq_card, ← Nat.card_perm]
    exact card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
apply : H.normalCore.index ∣ H.index
⊢ H.normalCore.index = H.index

Tactic:
apply dvd_antisymm _ (index_dvd_of_le H.normalCore_le)

Premises used: dvd_antisymm, Subgroup.index_dvd_of_le, Subgroup.normalCore_le
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
rwa : H.normalCore.index.Coprime (H.index - 1)!
⊢ H.normalCore.index ∣ H.index

Tactic:
rwa [← Coprime.dvd_mul_right, mul_factorial_pred hp.ne_zero]

Premises used: Nat.Coprime.dvd_mul_right, Nat.Prime.ne_zero, Nat.mul_factorial_pred
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index ≠ 1

Tactic:
have hr1 : H.normalCore.index ≠ 1 := fun hr1 ↦ hp.ne_one <|
    Nat.eq_one_of_dvd_one (hr1 ▸ H.normalCore.index_dvd_of_le H.normalCore_le)
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
rw : H.index - 1 < H.normalCore.index.minFac
⊢ H.normalCore.index.Coprime (H.index - 1)!

Tactic:
rw [Nat.coprime_factorial_iff hr1]

Premises used: Nat.coprime_factorial_iff
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.index - 1 < H.normalCore.index.minFac

Tactic:
lt_of_lt_of_le (Nat.sub_one_lt hp.ne_zero) <|
    hHp ▸ minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
      (dvd_trans (minFac_dvd H.normalCore.index) (H.normalCore.index_dvd_card))

Premises used: Nat.sub_one_lt, Nat.minFac_le_of_dvd, Eq.rec, Nat.minFac_dvd, dvd_trans, Nat.Prime.ne_zero, Subgroup.index, Nat.Prime.two_le, Subgroup.normalCore, Eq.symm, Nat.minFac_prime, lt_of_lt_of_le, Subgroup.index_dvd_card
-- Module: Mathlib.GroupTheory.IndexNormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.index - 1 < H.normalCore.index.minFac

Tactic:
exact lt_of_lt_of_le (Nat.sub_one_lt hp.ne_zero) <|
    hHp ▸ minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
      (dvd_trans (minFac_dvd H.normalCore.index) (H.normalCore.index_dvd_card))

Premises used: Nat.sub_one_lt, Nat.Prime.ne_zero, lt_of_lt_of_le
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
⊢ IsPerfect G ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤

Tactic:
⟨fun h ↦ h.commutator_eq_top, fun h ↦ ⟨h⟩⟩

Premises used: Group.IsPerfect.commutator_eq_top, Iff.intro, Group.IsPerfect.mk
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : Eq.{u_1 + 1} (α := Subgroup ↥H) (_root_.commutator ↥H) ⊤ ↔ ⁅H, H⁆ = H
rw₁ : map H.subtype (_root_.commutator ↥H) = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
rw₂ : ⁅H, H⁆ = map H.subtype ⊤ ↔ ⁅H, H⁆ = H
rw₃ : ⁅H, H⁆ = H.subtype.range ↔ ⁅H, H⁆ = H
rw₄ rw₅ : ⁅H, H⁆ = H ↔ ⁅H, H⁆ = H
⊢ IsPerfect.{u_1} ↥H ↔ ⁅H, H⁆ = H

Tactic:
rw [Group.isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, range_subtype]

Premises used: Subgroup.map_subtype_inj, Group.isPerfect_def, MonoidHom.range_eq_map, Subgroup.range_subtype, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPerfect.{u_1} ↥H
⊢ ⁅H, H⁆ = H

Tactic:
isPerfect_iff.mp hH

Premises used: Subgroup.isPerfect_iff, Iff.mp
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
hP : IsPerfect G
g : G
⊢ Membership.mem (γ := Subgroup G) (_root_.commutator G) g

Tactic:
simp
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
rw : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ IsPerfect G
rw₁ : Eq.{u_1 + 1} (α := Subgroup ↥⊤) (_root_.commutator ↥⊤) ⊤ ↔ Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₂ :
  Eq.{u_1 + 1} (α := Subgroup G) (map (G := ↥⊤) (Subgroup.subtype ⊤) (_root_.commutator ↥⊤))
      (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₃ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) (map (G := ↥⊤) (Subgroup.subtype ⊤) ⊤) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₄ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤)
      (MonoidHom.range (G := ↥⊤) (Subgroup.subtype ⊤)) ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₅ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤ ↔
    Eq (α := Subgroup G) (_root_.commutator G) ⊤
rw₆ rw₇ :
  Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤ ↔
    Eq.{u_1 + 1} (α := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ ⊤) ⊤
⊢ IsPerfect.{u_1} ↥⊤ ↔ IsPerfect G

Tactic:
rw [isPerfect_def, isPerfect_def, ← map_subtype_inj,
    map_subtype_commutator, ← MonoidHom.range_eq_map, subtype_range, commutator_def]

Premises used: Subgroup.map_subtype_inj, Group.isPerfect_def, MonoidHom.range_eq_map, Subgroup.subtype_range, commutator_def, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
f : G →* G'
inst_2 : IsPerfect G
⊢ IsPerfect.{u_1} ↥⊤

Tactic:
top_iff.mpr inferInstance

Premises used: Iff.mpr, Group.IsPerfect.top_iff, inferInstance
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
inst_2 : IsPerfect G
h : IsSolvable G
⊢ False

Tactic:
(h.commutator_lt_top_of_nontrivial G).ne commutator_eq_top

Premises used: IsSolvable.commutator_lt_top_of_nontrivial, Group.IsPerfect.commutator_eq_top, LT.lt.ne
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
inst_2 : IsPerfect G
h : IsSolvable G
⊢ False

Tactic:
exact (h.commutator_lt_top_of_nontrivial G).ne commutator_eq_top

Premises used: IsSolvable.commutator_lt_top_of_nontrivial, Group.IsPerfect.commutator_eq_top, LT.lt.ne
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
inst_2 : IsPerfect G
⊢ ¬IsNilpotent G

Tactic:
fun _ ↦ (not_isSolvable G) IsNilpotent.to_isSolvable

Premises used: Group.IsPerfect.not_isSolvable, IsNilpotent.to_isSolvable, Not
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
inst : Group G
inst_1 : Nontrivial G
inst_2 : IsPerfect G
⊢ ¬IsMulCommutative G

Tactic:
fun _ ↦ (not_isSolvable G) CommGroup.isSolvable

Premises used: Group.IsPerfect.not_isSolvable, CommGroup.isSolvable, Not
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
f : G →* G'
hG : IsPerfect G
h_comm : IsMulCommutative G
by_contra! : ∀ (h_not_subsingleton : Nontrivial G), False
⊢ Subsingleton G

Tactic:
by_contra! h_not_subsingleton
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
f : G →* G'
hG : IsPerfect G
h_comm : IsMulCommutative G
h_not_subsingleton : Nontrivial G
⊢ False

Tactic:
not_isMulCommutative G h_comm

Premises used: Group.IsPerfect.not_isMulCommutative
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
f : G →* G'
hG : IsPerfect G
h_comm : IsMulCommutative G
h_not_subsingleton : Nontrivial G
⊢ False

Tactic:
exact not_isMulCommutative G h_comm

Premises used: Group.IsPerfect.not_isMulCommutative
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H : Subgroup G
f : G →* G'
inst_2 : IsPerfect.{u_1} ↥H
rw : ⁅map f H, map f H⁆ = map f H
rw₁ : map f ⁅H, H⁆ = map f H
rw₂ rw₃ : map f H = map f H
⊢ IsPerfect.{u_2} ↥(map f H)

Tactic:
rw [isPerfect_iff, ← map_commutator, commutator_eq_self]

Premises used: Subgroup.commutator_eq_self, Subgroup.isPerfect_iff, Subgroup.map_commutator
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : IsPerfect G
rw : IsPerfect.{u_2} ↥(map f ⊤)
⊢ IsPerfect.{u_2} ↥f.range

Tactic:
rw [MonoidHom.range_eq_map]

Premises used: MonoidHom.range_eq_map
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : IsPerfect G
⊢ IsPerfect.{u_2} ↥(map f ⊤)

Tactic:
IsPerfect.map _

Premises used: Group.IsPerfect.map
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : IsPerfect G
⊢ IsPerfect.{u_2} ↥(map f ⊤)

Tactic:
exact IsPerfect.map _

Premises used: Group.IsPerfect.map
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : IsPerfect G
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
rw : IsPerfect.{u_2} ↥f.range
⊢ IsPerfect G'

Tactic:
rw [← top_iff, ← MonoidHom.range_eq_top_of_surjective f hf]

Premises used: Group.IsPerfect.top_iff, MonoidHom.range_eq_top_of_surjective
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
f : G →* G'
inst_2 : IsPerfect G
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := G') (⇑f : (a : G) → G')
⊢ IsPerfect.{u_2} ↥f.range

Tactic:
IsPerfect.range f

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

Tactic:
exact IsPerfect.range f

Premises used: Group.IsPerfect.range
-- Module: Mathlib.GroupTheory.IsPerfect
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H K : Subgroup G
f : G →* G'
inst_2 : H.Normal
inst_3 : IsPerfect G
⊢ IsPerfect.{u_1} (G ⧸ H)

Tactic:
ofSurjective (QuotientGroup.mk'_surjective H)

Premises used: Group.IsPerfect.ofSurjective, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hn : H.Normal
⊢ H.IsSubnormal

Tactic:
IsSubnormal.step _ ⊤ le_top IsSubnormal.top normal_subgroupOf

Premises used: Subgroup.normal_subgroupOf, Subgroup.IsSubnormal.step, le_top, Subgroup.IsSubnormal.top, Top.top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
⊢ IsSubnormal.{u_1} (G := G) ⊥

Tactic:
normal_bot.isSubnormal

Premises used: Subgroup.normal_bot, Subgroup.Normal.isSubnormal
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : IsSimpleGroup G
⊢ Normal.{u_1} (G := G) ⊤

Tactic:
simp
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
hG : IsSimpleGroup G
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
Knorm : K.Normal
step :
  ∀ (h_le : H ≤ ⊥) (hSubn : IsSubnormal.{u_1} (G := G) ⊥) (hN : Normal (G := ↥⊥) (H.subgroupOf ⊥))
    (Knorm : Normal.{u_1} (G := G) ⊥), H.Normal
step₁ :
  ∀ (h_le : H ≤ ⊤) (hSubn : IsSubnormal.{u_1} (G := G) ⊤) (hN : Normal (G := ↥⊤) (H.subgroupOf ⊤))
    (Knorm : Normal.{u_1} (G := G) ⊤), H.Normal
⊢ H.Normal

Tactic:
obtain rfl | rfl := Knorm.eq_bot_or_eq_top

Premises used: Subgroup.Normal.eq_bot_or_eq_top, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊥
hSubn : IsSubnormal.{u_1} (G := G) ⊥
hN : Normal (G := ↥⊥) (H.subgroupOf ⊥)
Knorm : Normal.{u_1} (G := G) ⊥
⊢ H.Normal

Tactic:
grind
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 : Subgroup G
hG : IsSimpleGroup G
H : Subgroup G
h_le : H ≤ ⊤
hSubn : IsSubnormal.{u_1} (G := G) ⊤
hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)
Knorm : Normal.{u_1} (G := G) ⊤
⊢ H.Normal

Tactic:
grind [!normal_subgroupOf_iff_le_normalizer_inf, inf_of_le_left, normalizer_eq_top_iff]

Premises used: inf_of_le_left, Subgroup.normal_subgroupOf_iff_le_normalizer_inf, Subgroup.normalizer_eq_top_iff
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : IsSimpleGroup G
hN : H.IsSubnormal
top : Normal.{u_1} (G := G) ⊤
step :
  ∀ (H K : Subgroup G) (h_le : H ≤ K) (hSubn : K.IsSubnormal) (hN : (H.subgroupOf K).Normal) (Knorm : K.Normal),
    H.Normal
⊢ H.Normal

Tactic:
induction hN with
  | top => simp
  | step H K h_le hSubn hN Knorm =>
    obtain rfl | rfl := Knorm.eq_bot_or_eq_top
    · grind
    · grind [!normal_subgroupOf_iff_le_normalizer_inf, inf_of_le_left, normalizer_eq_top_iff]

Premises used: inf_of_le_left, Subgroup.normal_subgroupOf_iff_le_normalizer_inf, Subgroup.IsSubnormal.step, Subgroup.normalizer_eq_top_iff, Subgroup.IsSubnormal.top, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hG : IsSimpleGroup G
hN : H.IsSubnormal
⊢ H = ⊥ ∨ H = ⊤

Tactic:
(hN.normal_of_isSimpleGroup hG).eq_bot_or_eq_top

Premises used: Subgroup.Normal.eq_bot_or_eq_top, Subgroup.IsSubnormal.normal_of_isSimpleGroup
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), ⊤ < K ∧ K.IsSubnormal ∧ (subgroupOf ⊤ K).Normal

Tactic:
simp
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : K = ⊤ ∨ ∃ (K_1 : Subgroup G), K < K_1 ∧ K_1.IsSubnormal ∧ (K.subgroupOf K_1).Normal
step :
  ∀ (HK : H ≤ ⊤) (hS : IsSubnormal.{u_1} (G := G) ⊤) (hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)),
    H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
step₁ :
  ∀ (K' : Subgroup G) (HK' : K < K') (hS' : K'.IsSubnormal) (hN' : (K.subgroupOf K').Normal),
    H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
obtain rfl | ⟨K', HK', hS', hN'⟩ := ih

Premises used: rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H : Subgroup G
HK : H ≤ ⊤
hS : IsSubnormal.{u_1} (G := G) ⊤
hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)
step :
  ∀ (HK : LE.le.{u_1} (α := Subgroup G) ⊤ ⊤) (hN : Normal.{u_1} (G := ↥⊤) (subgroupOf ⊤ ⊤)),
    Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), ⊤ < K ∧ K.IsSubnormal ∧ (subgroupOf ⊤ K).Normal
step₁ : ∀ (hH : H ≠ ⊤), H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
obtain rfl | hH := eq_or_ne H ⊤

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
hS : IsSubnormal.{u_1} (G := G) ⊤
HK : LE.le.{u_1} (α := Subgroup G) ⊤ ⊤
hN : Normal.{u_1} (G := ↥⊤) (subgroupOf ⊤ ⊤)
⊢ Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤ ∨ ∃ (K : Subgroup G), ⊤ < K ∧ K.IsSubnormal ∧ (subgroupOf ⊤ K).Normal

Tactic:
simp
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H : Subgroup G
HK : H ≤ ⊤
hS : IsSubnormal.{u_1} (G := G) ⊤
hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)
hH : H ≠ ⊤
⊢ H < ⊤ ∧ IsSubnormal.{u_1} (G := G) ⊤ ∧ Normal (G := ↥⊤) (H.subgroupOf ⊤)

Tactic:
simp [hH.lt_top , *]

Premises used: Ne.lt_top
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H : Subgroup G
HK : H ≤ ⊤
hS : IsSubnormal.{u_1} (G := G) ⊤
hN : Normal (G := ↥⊤) (H.subgroupOf ⊤)
hH : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
exact Or.inr ⟨⊤, by simp [hH.lt_top , *]⟩

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
step : ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ H = ⊤ ∨ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
right
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
step :
  ∀ (HK : H ≤ H) (hS : H.IsSubnormal) (hN : (H.subgroupOf H).Normal) (HK' : H < K') (hN' : (H.subgroupOf K').Normal),
    ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
step₁ : ∀ (hH : H ≠ K), ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
⊢ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
obtain rfl | hH := eq_or_ne H K

Premises used: eq_or_ne, rfl
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H K' : Subgroup G
hS' : K'.IsSubnormal
HK : H ≤ H
hS : H.IsSubnormal
hN : (H.subgroupOf H).Normal
HK' : H < K'
hN' : (H.subgroupOf K').Normal
w : Subgroup G
h : H < K' ∧ K'.IsSubnormal ∧ (H.subgroupOf K').Normal
⊢ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
use K'
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
hH : H ≠ K
⊢ H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
simpa [*] using HK.lt_of_ne hH

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.GroupTheory.IsSubnormal
Goal:
G : Type u_1
inst : Group G
H_1 H K : Subgroup G
HK : H ≤ K
hS : K.IsSubnormal
hN : (H.subgroupOf K).Normal
K' : Subgroup G
HK' : K < K'
hS' : K'.IsSubnormal
hN' : (K.subgroupOf K').Normal
hH : H ≠ K
⊢ ∃ (K : Subgroup G), H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
exact ⟨K, by simpa [*] using HK.lt_of_ne hH⟩