awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₇ : N.relIndex K = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₈ : N.relIndex (K ⊔ N) = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₉ : N.relIndex ⊤ = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ Nat.card.{u} ↥(map K.subtype H) = N.index
have rw₁₀ : N.index = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have hH₁ : 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]
Cleared hypotheses: hH
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
have rw : Nat.card.{u} ↥N * N.index = Nat.card G
Tactic: rw [hH, ← N.index_mul_card, mul_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G
have rw₁ : Nat.card.{u} ↥N * N.index = N.index * Nat.card.{u} ↥N
Tactic: rw [hH, ← N.index_mul_card, mul_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ Nat.card.{u} ↥N * Nat.card.{u} ↥(map K.subtype H) = Nat.card G
have rw₂ : N.index * Nat.card.{u} ↥N = N.index * Nat.card.{u} ↥N
Tactic: rw [hH, ← N.index_mul_card, mul_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have h7 : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have h8 : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ K = ⊥ ∨ K = N
have this : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
Tactic: have : Function.Surjective (QuotientGroup.mk' K) := Quotient.mk''_surjective
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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 = ⊥ ∨ K = N
have h4 : ∀ (K : Subgroup G) (hK : K ⊔ N = ⊤), K = ⊤
Tactic: have h4 := step1 h1 h2 h3
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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 = ⊤
⊢ K = ⊥ ∨ K = N
have contrapose! : ∀ (h4 : K ≠ ⊥ ∧ K ≠ N), ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
Tactic: contrapose! h4
Cleared hypotheses: h4
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
have rw : K.index < K.index * Nat.card.{u} ↥K
Tactic: rw [← index_eq_card, ← K.index_mul_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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 : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
have h5 : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
have index_map : index (map (QuotientGroup.mk' K) N) = N.index
Tactic: have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
have index_pos : 0 < N.index
Tactic: have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
have rw : (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime N.index
Tactic: rw [index_map]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime N.index
have refine : Nat.card.{u} ↥(map (QuotientGroup.mk' K) N) ∣ Nat.card.{u} ↥N
Tactic: refine h1.coprime_dvd_left ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
⊢ Nat.card.{u} ↥(map (QuotientGroup.mk' K) N) ∣ Nat.card.{u} ↥N
have rw : Nat.card.{u} (G ⧸ K) ∣ Nat.card G
Tactic: rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
have h6 : (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
Tactic: have h6 :
    (Nat.card (N.map (QuotientGroup.mk' K))).Coprime (N.map (QuotientGroup.mk' K)).index := by
    have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
    have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
    rw [index_map]
    refine h1.coprime_dvd_left ?_
    rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]
    exact K.card_quotient_dvd_card
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
h6 : (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
⊢ ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
have obtain : ∀ (H : Subgroup (G ⧸ K)) (hH : IsComplement' (map (QuotientGroup.mk' K) N) H), ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
Tactic: obtain ⟨H, hH⟩ := h2 (G ⧸ K) h5 h6
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
h6 : (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
have refine_1 : comap (QuotientGroup.mk' K) H ⊔ N = ⊤
Tactic: refine ⟨H.comap (QuotientGroup.mk' K), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
h6 : (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
refine_1 : comap (QuotientGroup.mk' K) H ⊔ N = ⊤
⊢ ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
have refine_2 : comap (QuotientGroup.mk' K) H ≠ ⊤
Tactic: refine ⟨H.comap (QuotientGroup.mk' K), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
h6 : (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
have refine : MonoidHom.ker (QuotientGroup.mk' K) ≤ N
Tactic: refine comap_map_eq_self ?_