G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
inst✝ : Normal ⊥
h1 : Nat.coprime (Fintype.card { x // x ∈ ⊥ }) (index ⊥)
h3 : ∀ (H : Subgroup G), ¬IsComplement' ⊥ H
⊢ False
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
N : Subgroup G
inst✝ : Normal N
h1 : Nat.coprime (Fintype.card { x // x ∈ N }) (index N)
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
h3 : ∀ (H : Subgroup G), ¬IsComplement' N H
⊢ N ≠ ⊥
rintro rfl
no goals
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Fintype G'],
    Fintype.card G' < Fintype.card G →
      ∀ {N' : Subgroup G'} [inst_2 : Normal N'],
        Nat.coprime (Fintype.card { x // x ∈ N' }) (index N') → ∃ H', IsComplement' N' H'
inst✝ : Normal ⊥
h1 : Nat.coprime (Fintype.card { x // x ∈ ⊥ }) (index ⊥)
h3 : ∀ (H : Subgroup G), ¬IsComplement' ⊥ H
⊢ False
exact h3 ⊤ isComplement'_bot_top