awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : IsMulCommutative.{u_1} ↥H
inst_2 : H.FiniteIndex
inst_3 : H.Normal
hH : (Nat.card.{u_1} ↥H).Coprime H.index
⊢ ∃ (K : Subgroup G), H.IsComplement' K

Tactic:
have ne : Nonempty (QuotientDiff H) := inferInstance
  ne.elim fun α => ⟨stabilizer G α, isComplement'_stabilizer_of_coprime hH⟩

Premises used: Nonempty.elim, inferInstance, Subgroup.isComplement'_stabilizer_of_coprime, Exists.intro, MulAction.stabilizer
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Normal.{u} (G := G) ⊥
h1 : (Nat.card.{u} ↥⊥).Coprime (index.{u} (G := G) ⊥)
h3 : ∀ (H : Subgroup G), ¬IsComplement' ⊥ H
⊢ False

Tactic:
h3 ⊤ isComplement'_bot_top

Premises used: Subgroup.isComplement'_bot_top, Top.top
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
inst_1 : Normal.{u} (G := G) ⊥
h1 : (Nat.card.{u} ↥⊥).Coprime (index.{u} (G := G) ⊥)
h3 : ∀ (H : Subgroup G), ¬IsComplement' ⊥ H
⊢ False

Tactic:
exact h3 ⊤ isComplement'_bot_top

Premises used: Subgroup.isComplement'_bot_top, Top.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
K : Subgroup G
hK : K ⊔ N = ⊤
contrapose! : ∀ (h3 : K ≠ ⊤), ∃ (H : Subgroup G), N.IsComplement' H
⊢ K = ⊤

Tactic:
contrapose! 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
rw : (comap K.subtype N).index = N.relIndex (K ⊔ N)
⊢ (comap K.subtype N).index = N.index

Tactic:
rw [← N.relIndex_top_right, ← hK]

Premises used: Subgroup.relIndex_top_right
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.relIndex (K ⊔ N)

Tactic:
(relIndex_sup_right K N).symm

Premises used: Subgroup.subgroupOf, Subgroup.relIndex_sup_right, Subgroup.relIndex, Eq.symm
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.relIndex (K ⊔ N)

Tactic:
exact (relIndex_sup_right K N).symm

Premises used: Subgroup.relIndex_sup_right, Eq.symm
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ (comap K.subtype N).index = N.index

Tactic:
have h4 : (N.comap K.subtype).index = N.index := by
    rw [← N.relIndex_top_right, ← hK]
    exact (relIndex_sup_right K N).symm
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
rw : Nat.card.{u} ↥K < K.index * Nat.card.{u} ↥K
⊢ Nat.card.{u} ↥K < Nat.card G

Tactic:
rw [← K.index_mul_card]

Premises used: Subgroup.index_mul_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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ Nat.card.{u} ↥K < K.index * Nat.card.{u} ↥K

Tactic:
lt_mul_of_one_lt_left Nat.card_pos (one_lt_index_of_ne_top h3)

Premises used: Nat.card_pos, Subgroup.one_lt_index_of_ne_top, lt_mul_of_one_lt_left
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ Nat.card.{u} ↥K < K.index * Nat.card.{u} ↥K

Tactic:
exact lt_mul_of_one_lt_left Nat.card_pos (one_lt_index_of_ne_top h3)

Premises used: Nat.card_pos, Subgroup.one_lt_index_of_ne_top, lt_mul_of_one_lt_left
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ Nat.card.{u} ↥K < Nat.card G

Tactic:
have h5 : Nat.card K < Nat.card G := by
    rw [← K.index_mul_card]
    exact lt_mul_of_one_lt_left Nat.card_pos (one_lt_index_of_ne_top 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
rw : (Nat.card.{u} ↥(comap K.subtype N)).Coprime N.index
⊢ (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index

Tactic:
rw [h4]
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
⊢ (Nat.card.{u} ↥(comap K.subtype N)).Coprime N.index

Tactic:
h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)

Premises used: Nat.Coprime.coprime_dvd_left, Subgroup.subtype, Subtype.coe_injective, Subgroup.card_comap_dvd_of_injective
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
⊢ (Nat.card.{u} ↥(comap K.subtype N)).Coprime N.index

Tactic:
exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)

Premises used: Nat.Coprime.coprime_dvd_left, Subgroup.subtype, Subtype.coe_injective, Subgroup.card_comap_dvd_of_injective
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
⊢ (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index

Tactic:
have h6 : Nat.Coprime (Nat.card (N.comap K.subtype)) (N.comap K.subtype).index := by
    rw [h4]
    exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
obtain : ∀ (H : Subgroup ↥K) (hH : (comap K.subtype N).IsComplement' H), ∃ (H : Subgroup G), N.IsComplement' H
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
obtain ⟨H, hH⟩ := h2 K h5 h6

Premises used: Membership.mem, 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
rw : relIndex ⊥ (map K.subtype H) = N.index
rw₁ : (comap K.subtype ⊥).relIndex H = N.index
rw₂ : K.subtype.ker.relIndex H = N.index
rw₃ : relIndex ⊥ H = N.index
rw₄ : Nat.card.{u} ↥H = N.index
rw₅ : (comap K.subtype N).index = N.index
rw₆ : N.relIndex K.subtype.range = N.index
rw₇ : N.relIndex K = N.index
rw₈ : N.relIndex (K ⊔ N) = N.index
rw₉ : N.relIndex ⊤ = N.index
rw₁₀ rw₁₁ : N.index = N.index
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index

Tactic:
rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]

Premises used: MonoidHom.comap_bot, Subgroup.IsComplement'.index_eq_card, Subgroup.ker_subtype, Subgroup.relIndex_sup_right, Subgroup.relIndex_bot_left, Subgroup.index_comap, Subgroup.relIndex_comap, Subgroup.IsComplement'.symm, Subgroup.range_subtype, Subgroup.relIndex_top_right
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : (comap K.subtype N).IsComplement' H
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index

Tactic:
replace hH : Nat.card (H.map K.subtype) = N.index := by
    rw [← relIndex_bot_left, ← relIndex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
      relIndex_bot_left, ← IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
      range_subtype, ← relIndex_sup_right, hK, relIndex_top_right]
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card.{u} ↥(map K.subtype H) = N.index
rw : Nat.card.{u} ↥N * N.index = Nat.card G
rw₁ : Nat.card.{u} ↥N * N.index = N.index * Nat.card.{u} ↥N
rw₂ rw₃ : N.index * Nat.card.{u} ↥N = N.index * Nat.card.{u} ↥N
⊢ Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G

Tactic:
rw [hH, ← N.index_mul_card, mul_comm]

Premises used: Subgroup.index_mul_card, mul_comm
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card.{u} ↥(map K.subtype H) = N.index
⊢ Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G

Tactic:
have h7 : Nat.card N * Nat.card (H.map K.subtype) = Nat.card G := by
    rw [hH, ← N.index_mul_card, mul_comm]
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card.{u} ↥(map K.subtype H) = N.index
h7 : Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G
rwa rwa₁ rwa₂ rwa₃ : (Nat.card.{u} ↥N).Coprime N.index
⊢ (Nat.card.{u} ↥N).Coprime (Nat.card.{u} ↥(map K.subtype H))

Tactic:
rwa [hH]
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card.{u} ↥(map K.subtype H) = N.index
h7 : Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G
⊢ (Nat.card.{u} ↥N).Coprime (Nat.card.{u} ↥(map K.subtype H))

Tactic:
have h8 : (Nat.card N).Coprime (Nat.card (H.map K.subtype)) := by
    rwa [hH]
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card.{u} ↥(map K.subtype H) = N.index
h7 : Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G
h8 : (Nat.card.{u} ↥N).Coprime (Nat.card.{u} ↥(map K.subtype H))
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
⟨H.map K.subtype, isComplement'_of_coprime h7 h8⟩

Premises used: Subgroup.map, Subgroup.subtype, Subgroup.isComplement'_of_coprime, Exists.intro
-- 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'
inst_2 : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card.{u} ↥K < Nat.card G
h6 : (Nat.card.{u} ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card.{u} ↥(map K.subtype H) = N.index
h7 : Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G
h8 : (Nat.card.{u} ↥N).Coprime (Nat.card.{u} ↥(map K.subtype H))
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
exact ⟨H.map K.subtype, isComplement'_of_coprime h7 h8⟩
-- 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 G
inst_3 : K.Normal
hK : K ≤ N
⊢ Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)

Tactic:
have : Function.Surjective (QuotientGroup.mk' K) := Quotient.mk''_surjective
-- 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 G
inst_3 : K.Normal
hK : K ≤ N
this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
⊢ ∀ (K : Subgroup G) (hK : K ⊔ N = ⊤), K = ⊤

Tactic:
have h4 := step1 h1 h2 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
K : Subgroup G
inst_3 : K.Normal
hK : K ≤ N
this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
h4 : ∀ (K : Subgroup G) (hK : K ⊔ N = ⊤), K = ⊤
contrapose! : ∀ (h4 : K ≠ ⊥ ∧ K ≠ N), ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
⊢ K = ⊥ ∨ K = N

Tactic:
contrapose! h4
-- 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 G
inst_3 : K.Normal
hK : K ≤ N
this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
h4 : K ≠ ⊥ ∧ K ≠ N
rw : K.index < K.index * Nat.card.{u} ↥K
⊢ Nat.card.{u} (G ⧸ K) < Nat.card G

Tactic:
rw [← index_eq_card, ← K.index_mul_card]

Premises used: Subgroup.index_mul_card, Subgroup.index_eq_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
K : Subgroup G
inst_3 : K.Normal
hK : K ≤ N
this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
h4 : K ≠ ⊥ ∧ K ≠ N
⊢ K.index < K.index * Nat.card.{u} ↥K

Tactic:
lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite)
        (K.one_lt_card_iff_ne_bot.mpr h4.1)

Premises used: Iff.mpr, Subgroup.index_ne_zero_of_finite, Subgroup.one_lt_card_iff_ne_bot, Nat.pos_of_ne_zero, And.left, lt_mul_of_one_lt_right
-- 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 G
inst_3 : K.Normal
hK : K ≤ N
this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
h4 : K ≠ ⊥ ∧ K ≠ N
⊢ K.index < K.index * Nat.card.{u} ↥K

Tactic:
refine
      lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite)
        (K.one_lt_card_iff_ne_bot.mpr h4.1)

Premises used: Iff.mpr, Subgroup.index_ne_zero_of_finite, Subgroup.one_lt_card_iff_ne_bot, Nat.pos_of_ne_zero, And.left, lt_mul_of_one_lt_right
-- 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 G
inst_3 : K.Normal
hK : K ≤ N
this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
h4 : K ≠ ⊥ ∧ K ≠ N
⊢ Nat.card.{u} (G ⧸ K) < Nat.card G

Tactic:
have h5 : Nat.card (G ⧸ K) < Nat.card G := by
    rw [← index_eq_card, ← K.index_mul_card]
    refine
      lt_mul_of_one_lt_right (Nat.pos_of_ne_zero index_ne_zero_of_finite)
        (K.one_lt_card_iff_ne_bot.mpr h4.1)
-- 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 G
inst_3 : K.Normal
hK : K ≤ N
this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
h4 : K ≠ ⊥ ∧ K ≠ N
h5 : Nat.card.{u} (G ⧸ K) < Nat.card G
rwa rwa₁ rwa₂ rwa₃ : K ≤ N
⊢ MonoidHom.ker (QuotientGroup.mk' K) ≤ N

Tactic:
rwa [QuotientGroup.ker_mk']

Premises used: QuotientGroup.ker_mk'