awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
K : Subgroup ↥N
inst_3 : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
⊢ map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = map N.subtype ⊤

Tactic:
conv at key =>
    rhs
    rhs
    rw [← N.range_subtype, N.subtype.range_eq_map]

Premises used: Subgroup.subtype, MonoidHom.range_eq_map, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
K : Subgroup ↥N
inst_3 : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = map N.subtype ⊤
rwa : ∀ (key : K = ⊥ ∨ map N.subtype K = map N.subtype ⊤), K = ⊥ ∨ K = ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (key : K = ⊥ ∨ K = ⊤), K = ⊥ ∨ K = ⊤
⊢ K = ⊥ ∨ K = ⊤

Tactic:
rwa [map_subtype_inj, map_subtype_inj] at key

Premises used: Subgroup.map_subtype_inj
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
⊢ Nat.Prime (Nat.card.{u} ↥N).minFac

Tactic:
Nat.minFac_prime (N.one_lt_card_iff_ne_bot.mpr (step0 h1 h3)).ne'

Premises used: Iff.mpr, Subgroup.one_lt_card_iff_ne_bot, _private.0.Subgroup.SchurZassenhausInduction.step0, LT.lt.ne', Nat.minFac_prime
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
⊢ Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)

Tactic:
haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
apply : (Nat.card.{u} ↥N).minFac ∣ Nat.card.{u} ↥N
⊢ (↑P : Subgroup ↥N) ≠ ⊥

Tactic:
apply P.ne_bot_of_dvd_card

Premises used: Sylow.ne_bot_of_dvd_card
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
⊢ (Nat.card.{u} ↥N).minFac ∣ Nat.card.{u} ↥N

Tactic:
(Nat.card N).minFac_dvd

Premises used: Membership.mem, Subtype, Nat.minFac_dvd, Nat.card
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
⊢ (Nat.card.{u} ↥N).minFac ∣ Nat.card.{u} ↥N

Tactic:
exact (Nat.card N).minFac_dvd

Premises used: Membership.mem, Subtype, Nat.minFac_dvd, Nat.card
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
⊢ Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)

Tactic:
haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
⊢ IsPGroup.{u} (Nat.card.{u} ↥N).minFac ↥N

Tactic:
Sylow.nonempty.elim fun P => P.2.of_surjective P.1.subtype ?_

Premises used: Sylow.isPGroup', Sylow.toSubgroup, IsPGroup.of_surjective, Nonempty.elim, Subgroup.subtype, Sylow.nonempty
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
refine :
  ∀ (P : Sylow (Nat.card.{u} ↥N).minFac ↥N),
    Function.Surjective (α := ↥(↑P : Subgroup ↥N)) (β := ↥N)
      (⇑(↑P : Subgroup ↥N).subtype : (a : ↥(↑P : Subgroup ↥N)) → ↥N)
⊢ IsPGroup.{u} (Nat.card.{u} ↥N).minFac ↥N

Tactic:
refine Sylow.nonempty.elim fun P => P.2.of_surjective P.1.subtype ?_

Premises used: Sylow.isPGroup', Sylow.toSubgroup, IsPGroup.of_surjective, Nonempty.elim, Subgroup.subtype, Sylow.nonempty
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
rw : (↑P : Subgroup ↥N) = ⊤
⊢ Function.Surjective (α := ↥(↑P : Subgroup ↥N)) (β := ↥N)
    (⇑(↑P : Subgroup ↥N).subtype : (a : ↥(↑P : Subgroup ↥N)) → ↥N)

Tactic:
rw [← MonoidHom.range_eq_top, range_subtype]

Premises used: MonoidHom.range_eq_top, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
⊢ (map N.subtype (↑P : Subgroup ↥N)).Normal

Tactic:
haveI : (P.1.map N.subtype).Normal :=
    normalizer_eq_top_iff.mp (step1 h1 h2 h3 _ P.normalizer_sup_eq_top)
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this_1 : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
this : (map N.subtype (↑P : Subgroup ↥N)).Normal
⊢ (↑P : Subgroup ↥N) = ⊤

Tactic:
(step3 h1 h2 h3 P.1).resolve_left (step5 h1 h3)

Premises used: Sylow.toSubgroup, _private.0.Subgroup.SchurZassenhausInduction.step3, Or.resolve_left, _private.0.Subgroup.SchurZassenhausInduction.step5
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this_1 : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
this : (map N.subtype (↑P : Subgroup ↥N)).Normal
⊢ (↑P : Subgroup ↥N) = ⊤

Tactic:
exact (step3 h1 h2 h3 P.1).resolve_left (step5 h1 h3)

Premises used: Sylow.toSubgroup, _private.0.Subgroup.SchurZassenhausInduction.step3, Or.resolve_left, _private.0.Subgroup.SchurZassenhausInduction.step5
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
⊢ Nontrivial.{u} ↥N

Tactic:
haveI := N.bot_or_nontrivial.resolve_left (step0 h1 h3)
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this : Nontrivial.{u} ↥N
⊢ Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)

Tactic:
haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this_1 : Nontrivial.{u} ↥N
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
⊢ IsMulCommutative.{u} ↥N

Tactic:
⟨⟨fun g h => ((eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left
      (step6 h1 h2 h3).bot_lt_center.ne') (mem_top h)).comm g).symm⟩⟩

Premises used: _private.0.Subgroup.SchurZassenhausInduction.step3, eq_top_iff, Membership.mem, Subtype, IsMulCentral.comm, Or.resolve_left, Subgroup.center, IsPGroup.bot_lt_center, LT.lt.ne', Commute.symm, Iff.mp, Subgroup.mem_top, _private.0.Subgroup.SchurZassenhausInduction.step6, IsMulCommutative.mk, Std.Commutative.mk
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
h1 : (Nat.card.{u} ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
this_1 : Nontrivial.{u} ↥N
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
⊢ IsMulCommutative.{u} ↥N

Tactic:
exact
    ⟨⟨fun g h => ((eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left
      (step6 h1 h2 h3).bot_lt_center.ne') (mem_top h)).comm g).symm⟩⟩
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
n : ℕ
G : Type u
inst : Group G
inst_1 : Finite G
hG : Nat.card G = n
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
revert :
  ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = n) {N : Subgroup G} [N.Normal]
    (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
revert G
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
n : ℕ
ih :
  ∀ m < n,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
⊢ ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = n) {N : Subgroup G} [N.Normal]
    (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
?_
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
n : ℕ
ind :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n,
        ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
          (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H)
    {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = n) {N : Subgroup G} [N.Normal]
    (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
⊢ ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = n) {N : Subgroup G} [N.Normal]
    (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
induction n using Nat.strongRecOn with | ind n ih => ?_
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
not_forall_not.mp fun h3 => ?_

Premises used: not_forall_not, Iff.mp
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
ind : ∀ (h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x), False
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
refine not_forall_not.mp fun h3 => ?_

Premises used: not_forall_not, Iff.mp
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x : Group G'
h : Finite G'
hG' : Nat.card G' < Nat.card G
apply : Nat.card G' = Nat.card G'
⊢ ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'

Tactic:
apply ih _ hG'
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x : Group G'
h : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ Nat.card G' = Nat.card G'

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
⊢ IsMulCommutative.{u} ↥N

Tactic:
haveI := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
this : IsMulCommutative.{u} ↥N
⊢ False

Tactic:
not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN)

Premises used: not_exists_of_forall_not, _private.0.Subgroup.exists_right_complement'_of_coprime_aux
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [Finite G] (hG : Nat.card G = m) {N : Subgroup G} [N.Normal]
      (hN : (Nat.card.{u} ↥N).Coprime N.index), ∃ (H : Subgroup G), N.IsComplement' H
N : Subgroup G
inst_2 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
this : IsMulCommutative.{u} ↥N
⊢ False

Tactic:
exact not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN)

Premises used: not_exists_of_forall_not, _private.0.Subgroup.exists_right_complement'_of_coprime_aux
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
pos : ∀ (hN1 : Nat.card.{u} ↥N = 0), ∃ (H : Subgroup G), N.IsComplement' H
neg : ∀ (hN1 : ¬Nat.card.{u} ↥N = 0), ∃ (H : Subgroup G), N.IsComplement' H
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
by_cases hN1 : Nat.card N = 0

Premises used: Membership.mem, Subtype, Nat.card
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : Nat.card.{u} ↥N = 0
⊢ N = ⊤

Tactic:
rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN

Premises used: Nat.coprime_zero_left, Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : Nat.card.{u} ↥N = 0
hN₁ : N = ⊤
⊢ Nat.card.{u} ↥N = 0

Tactic:
rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN

Premises used: Nat.coprime_zero_left, Subgroup.index_eq_one
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : N = ⊤
hN1 : Nat.card.{u} ↥N = 0
pos : ∃ (H : Subgroup G), IsComplement' ⊤ H
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
rw [hN]
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : N = ⊤
hN1 : Nat.card.{u} ↥N = 0
⊢ ∃ (H : Subgroup G), IsComplement' ⊤ H

Tactic:
⟨⊥, isComplement'_top_bot⟩

Premises used: Bot.bot, Subgroup.isComplement'_top_bot, Exists.intro
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : N = ⊤
hN1 : Nat.card.{u} ↥N = 0
⊢ ∃ (H : Subgroup G), IsComplement' ⊤ H

Tactic:
exact ⟨⊥, isComplement'_top_bot⟩
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
pos : ∀ (hN2 : N.index = 0), ∃ (H : Subgroup G), N.IsComplement' H
neg : ∀ (hN2 : ¬N.index = 0), ∃ (H : Subgroup G), N.IsComplement' H
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
by_cases hN2 : N.index = 0

Premises used: Subgroup.index
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
⊢ Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N

Tactic:
rw [hN2, Nat.coprime_zero_right, Nat.card_eq_one_iff_unique] at hN

Premises used: Nat.coprime_zero_right, Nat.card_eq_one_iff_unique
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
hN₁ : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
⊢ ¬Nat.card.{u} ↥N = 0

Tactic:
rw [hN2, Nat.coprime_zero_right, Nat.card_eq_one_iff_unique] at hN

Premises used: Nat.coprime_zero_right, Nat.card_eq_one_iff_unique
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
hN₁ : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
hN1₁ : ¬Nat.card.{u} ↥N = 0
⊢ N.index = 0

Tactic:
rw [hN2, Nat.coprime_zero_right, Nat.card_eq_one_iff_unique] at hN

Premises used: Nat.coprime_zero_right, Nat.card_eq_one_iff_unique
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
⊢ Subsingleton.{u + 1} ↥N

Tactic:
have := hN.1
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
this : Subsingleton.{u + 1} ↥N
pos : ∃ (H : Subgroup G), IsComplement' ⊥ H
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
rw [N.eq_bot_of_subsingleton]

Premises used: Subgroup.eq_bot_of_subsingleton
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
this : Subsingleton.{u + 1} ↥N
⊢ ∃ (H : Subgroup G), IsComplement' ⊥ H

Tactic:
⟨⊤, isComplement'_bot_top⟩

Premises used: Exists.intro, Subgroup.isComplement'_bot_top, Top.top
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
this : Subsingleton.{u + 1} ↥N
⊢ ∃ (H : Subgroup G), IsComplement' ⊥ H

Tactic:
exact ⟨⊤, isComplement'_bot_top⟩
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
h : Nat.card G ≠ 0
⊢ Finite G

Tactic:
apply Nat.finite_of_card_ne_zero

Premises used: Nat.finite_of_card_ne_zero
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
h : Nat.card.{u} ↥N * N.index ≠ 0
⊢ Nat.card G ≠ 0

Tactic:
rw [← N.card_mul_index]

Premises used: Subgroup.card_mul_index
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card.{u} ↥N * N.index ≠ 0

Tactic:
mul_ne_zero hN1 hN2

Premises used: mul_ne_zero
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card.{u} ↥N * N.index ≠ 0

Tactic:
exact mul_ne_zero hN1 hN2

Premises used: mul_ne_zero
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
⊢ Finite G

Tactic:
have hN3 : Finite G := by
    apply Nat.finite_of_card_ne_zero
    rw [← N.card_mul_index]
    exact mul_ne_zero hN1 hN2
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
hN3 : Finite G
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
exists_right_complement'_of_coprime_aux' rfl hN

Premises used: _private.0.Subgroup.exists_right_complement'_of_coprime_aux', rfl