n : ℕ
⊢ ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
    Fintype.card G = n →
      ∀ {N : Subgroup G} [inst_2 : Normal N],
        Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
hG : Fintype.card G = n
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
⊢ ∃ H, IsComplement' N H
revert G
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n →
          ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
            Fintype.card G = m →
              ∀ {N : Subgroup G} [inst_2 : Normal N],
                Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H) →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = n →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
n : ℕ
⊢ ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
    Fintype.card G = n →
      ∀ {N : Subgroup G} [inst_2 : Normal N],
        Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
apply Nat.strongInductionOn n
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
⊢ ∃ H, IsComplement' N H
n : ℕ
⊢ ∀ (n : ℕ),
    (∀ (m : ℕ),
        m < n →
          ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
            Fintype.card G = m →
              ∀ {N : Subgroup G} [inst_2 : Normal N],
                Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H) →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = n →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
rintro n ih G _ _ rfl N _ hN
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
⊢ False
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
⊢ ∃ H, IsComplement' N H
refine' not_forall_not.mp fun h3 => _
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
this : IsCommutative N
⊢ False
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
⊢ False
haveI := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
this : IsCommutative N
⊢ False
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
this : IsCommutative N
⊢ False
rw [← Nat.card_eq_fintype_card] at hN
no goals
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Nat.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
this : IsCommutative N
⊢ False
exact not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN)
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
G' : Type u
x✝¹ : Group G'
x✝ : Fintype G'
hG' : Fintype.card G' < Fintype.card G
⊢ Fintype.card G' = Fintype.card G'
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
G' : Type u
x✝¹ : Group G'
x✝ : Fintype G'
hG' : Fintype.card G' < Fintype.card G
⊢ ∀ {N' : Subgroup G'} [inst : Normal N'],
    Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
apply ih _ hG'
no goals
n : ℕ
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
ih :
  ∀ (m : ℕ),
    m < Fintype.card G →
      ∀ {G : Type u} [inst : Group G] [inst_1 : Fintype G],
        Fintype.card G = m →
          ∀ {N : Subgroup G} [inst_2 : Normal N],
            Nat.coprime (Fintype.card { x // x ∈ N }) (index N) → ∃ H, IsComplement' N H
N : Subgroup G
inst✝ : Normal N
hN : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h3 : ∀ (x : Subgroup G), ¬IsComplement' N x
G' : Type u
x✝¹ : Group G'
x✝ : Fintype G'
hG' : Fintype.card G' < Fintype.card G
⊢ Fintype.card G' = Fintype.card G'
rfl