awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) H ⊔ N = ⊤
have key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
Tactic: have key : (N.map (QuotientGroup.mk' K)).comap (QuotientGroup.mk' K) = N := by
      refine comap_map_eq_self ?_
      rwa [QuotientGroup.ker_mk']
-- 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
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤
have refine_1 : comap (QuotientGroup.mk' K) H ⊔ comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = ⊤
Tactic: rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]
-- 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
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
refine_1 : comap (QuotientGroup.mk' K) H ⊔ comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = ⊤
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤
have refine_1₁ : comap (QuotientGroup.mk' K) (H ⊔ map (QuotientGroup.mk' K) N) = ⊤
Tactic: rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]
-- 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
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
refine_1 : comap (QuotientGroup.mk' K) H ⊔ comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = ⊤
refine_1₁ : comap (QuotientGroup.mk' K) (H ⊔ map (QuotientGroup.mk' K) N) = ⊤
refine_1₂ : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤
have refine_1₃ : comap (QuotientGroup.mk' K) ⊤ = ⊤
Tactic: rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]
-- 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
key : comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N
refine_1 : comap (QuotientGroup.mk' K) H ⊔ comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = ⊤
refine_1₁ : comap (QuotientGroup.mk' K) (H ⊔ map (QuotientGroup.mk' K) N) = ⊤
refine_1₂ : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
refine_1₃ : comap (QuotientGroup.mk' K) ⊤ = ⊤
refine_1₄ : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤
have refine_1₅ : Eq.{u + 1} (α := Subgroup G) ⊤ ⊤
Tactic: rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]
-- 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
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
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False
have hH₁ : N ≤ K
Tactic: rw [comap_injective this hH', isComplement'_top_right, map_eq_bot_iff,
      QuotientGroup.ker_mk'] at hH
Cleared hypotheses: hH, 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 ↥N
inst_3 : (map N.subtype K).Normal
⊢ K = ⊥ ∨ K = ⊤
have key : map N.subtype K = ⊥ ∨ map N.subtype K = N
Tactic: have key := step2 h1 h2 h3 (K.map N.subtype) (map_subtype_le K)
-- 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 ↥N
inst_3 : (map N.subtype K).Normal
key : map N.subtype K = ⊥ ∨ map N.subtype K = N
⊢ K = ⊥ ∨ K = ⊤
have key₁ : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
Tactic: rw [← map_bot N.subtype] at key
Cleared hypotheses: key
-- 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 ↥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 = N
have rhs : map N.subtype K = N
Tactic: rhs
-- 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 ↥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 = N
have rhs : N
Tactic: rhs
-- 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 ↥N
inst_3 : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
| N
have rw : map N.subtype ⊤
Tactic: rw [← N.range_subtype, N.subtype.range_eq_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 ↥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 = N
have rw : map N.subtype ⊤
Tactic: rhs
    rhs
    rw [← N.range_subtype, N.subtype.range_eq_map]
-- 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 ↥N
inst_3 : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N
⊢ K = ⊥ ∨ K = ⊤
have key₁ : 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]
Cleared hypotheses: key
-- 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 ↥N
inst_3 : (map N.subtype K).Normal
key : map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = map N.subtype ⊤
⊢ K = ⊥ ∨ K = ⊤
have rwa : ∀ (key : K = ⊥ ∨ map N.subtype K = map N.subtype ⊤), K = ⊥ ∨ K = ⊤
Tactic: rwa [map_subtype_inj, map_subtype_inj] at key
Cleared hypotheses: key
-- 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 ↥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 = ⊤
⊢ K = ⊥ ∨ K = ⊤
have rwa₁ : ∀ (key : K = ⊥ ∨ K = ⊤), K = ⊥ ∨ K = ⊤
Tactic: rwa [map_subtype_inj, map_subtype_inj] at key
Cleared hypotheses: key
-- 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
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst_2 : Finite G
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
⊢ (↑P : Subgroup ↥N) ≠ ⊥
have this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
Tactic: haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 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
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)
⊢ (↑P : Subgroup ↥N) ≠ ⊥
have apply : (Nat.card.{u} ↥N).minFac ∣ Nat.card.{u} ↥N
Tactic: apply P.ne_bot_of_dvd_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
⊢ IsPGroup.{u} (Nat.card.{u} ↥N).minFac ↥N
have this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
Tactic: haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 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
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
⊢ IsPGroup.{u} (Nat.card.{u} ↥N).minFac ↥N
have refine : ∀ (P : Sylow (Nat.card.{u} ↥N).minFac ↥N),
  Function.Surjective (α := ↥(↑P : Subgroup ↥N)) (β := ↥N)
    (⇑(↑P : Subgroup ↥N).subtype : (a : ↥(↑P : Subgroup ↥N)) → ↥N)
Tactic: refine Sylow.nonempty.elim fun P => P.2.of_surjective P.1.subtype ?_
-- 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
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
⊢ Function.Surjective (α := ↥(↑P : Subgroup ↥N)) (β := ↥N)
    (⇑(↑P : Subgroup ↥N).subtype : (a : ↥(↑P : Subgroup ↥N)) → ↥N)
have rw : (↑P : Subgroup ↥N) = ⊤
Tactic: rw [← MonoidHom.range_eq_top, range_subtype]
-- 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
this : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
P : Sylow (Nat.card.{u} ↥N).minFac ↥N
⊢ (↑P : Subgroup ↥N) = ⊤
have this₁ : (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)
-- 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
⊢ IsMulCommutative.{u} ↥N
have this : Nontrivial.{u} ↥N
Tactic: haveI := N.bot_or_nontrivial.resolve_left (step0 h1 h3)
-- 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
this : Nontrivial.{u} ↥N
⊢ IsMulCommutative.{u} ↥N
have this₁ : Fact (Nat.Prime (Nat.card.{u} ↥N).minFac)
Tactic: haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have 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
Tactic: revert G
Cleared hypotheses: G, inst, inst_1, hG, N, inst_2, hN
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
n : ℕ
⊢ ∀ {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
have 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
Tactic: induction n using Nat.strongRecOn with | ind n ih => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
have ind : ∀ (h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x), False
Tactic: refine not_forall_not.mp fun h3 => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card.{u} ↥N').Coprime N'.index → ∃ (H' : Subgroup G'), N'.IsComplement' H'
have apply : Nat.card G' = Nat.card G'
Tactic: apply ih _ hG'
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ False
have this : IsMulCommutative.{u} ↥N
Tactic: haveI := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have pos : ∀ (hN1 : Nat.card.{u} ↥N = 0), ∃ (H : Subgroup G), N.IsComplement' H
Tactic: by_cases hN1 : Nat.card N = 0
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have neg : ∀ (hN1 : ¬Nat.card.{u} ↥N = 0), ∃ (H : Subgroup G), N.IsComplement' H
Tactic: by_cases hN1 : Nat.card N = 0
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have hN₁ : N = ⊤
Tactic: rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN
Cleared hypotheses: hN, hN1
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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), N.IsComplement' H
have pos : ∃ (H : Subgroup G), IsComplement' ⊤ H
Tactic: rw [hN]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have pos : ∀ (hN2 : N.index = 0), ∃ (H : Subgroup G), N.IsComplement' H
Tactic: by_cases hN2 : N.index = 0
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have neg : ∀ (hN2 : ¬N.index = 0), ∃ (H : Subgroup G), N.IsComplement' H
Tactic: by_cases hN2 : N.index = 0
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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 : Subgroup G), N.IsComplement' H
have hN₁ : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
Tactic: rw [hN2, Nat.coprime_zero_right, Nat.card_eq_one_iff_unique] at hN
Cleared hypotheses: hN, hN1, hN2
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
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
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have this : Subsingleton.{u + 1} ↥N
Tactic: have := hN.1