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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
⊢ K = ⊥ ∨ K = N
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
⊢ K = ⊥ ∨ K = N
have : Function.Surjective (QuotientGroup.mk' K) := Quotient.surjective_Quotient_mk''
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ∀ (K : Subgroup G), K ⊔ N = ⊤ → K = ⊤
⊢ K = ⊥ ∨ K = N
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
⊢ K = ⊥ ∨ K = N
have h4 := step1 h1 h2 h3
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬(K = ⊥ ∨ K = N)
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ∀ (K : Subgroup G), K ⊔ N = ⊤ → K = ⊤
⊢ K = ⊥ ∨ K = N
contrapose! h4
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬(K = ⊥ ∨ K = N)
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
rw [not_or] at h4
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
have h5 : Fintype.card (G ⧸ K) < Fintype.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)
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
have h6 :
  (Fintype.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
case intro
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
obtain ⟨H, hH⟩ := h2 (G ⧸ K) h5 h6
case intro.refine'_1
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤

case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ≠ ⊤
case intro
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ ∃ K, K ⊔ N = ⊤ ∧ K ≠ ⊤
refine' ⟨H.comap (QuotientGroup.mk' K), _, _⟩
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
⊢ index K < index K * Fintype.card { x // x ∈ K }
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
⊢ Fintype.card (G ⧸ K) < Fintype.card G
rw [← index_eq_card, ← K.index_mul_card]
no goals
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
⊢ index K < index K * Fintype.card { x // x ∈ K }
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)
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index N)
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
rw [index_map]
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N } ∣ Fintype.card { x // x ∈ N }
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index N)
refine' h1.coprime_dvd_left _
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Fintype.card (G ⧸ K) ∣ Fintype.card G
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N } ∣ Fintype.card { x // x ∈ N }
rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]
no goals
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
index_map : index (map (QuotientGroup.mk' K) N) = index N
index_pos : 0 < index N
⊢ Fintype.card (G ⧸ K) ∣ Fintype.card G
exact K.card_quotient_dvd_card
no goals
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
⊢ MonoidHom.ker (QuotientGroup.mk' K) ≤ N
rwa [QuotientGroup.ker_mk']
case intro.refine'_1
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (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 = ⊤
case intro.refine'_1
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (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 : (N.map (QuotientGroup.mk' K)).comap (QuotientGroup.mk' K) = N := by
  refine' comap_map_eq_self _
  rwa [QuotientGroup.ker_mk']
no goals
case intro.refine'_1
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (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 = ⊤
rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ MonoidHom.ker (QuotientGroup.mk' K) ≤ N
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (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
refine' comap_map_eq_self _
no goals
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ MonoidHom.ker (QuotientGroup.mk' K) ≤ N
rwa [QuotientGroup.ker_mk']
case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ≠ comap (QuotientGroup.mk' K) ⊤
case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ≠ ⊤
rw [← comap_top (QuotientGroup.mk' K)]
case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (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
case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : IsComplement' (map (QuotientGroup.mk' K) N) H
⊢ comap (QuotientGroup.mk' K) H ≠ comap (QuotientGroup.mk' K) ⊤
intro hH'
case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : N ≤ K
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False
case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (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
rw [comap_injective this hH', isComplement'_top_right, map_eq_bot_iff,
  QuotientGroup.ker_mk'] at hH
no goals
case intro.refine'_2
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
K : Subgroup G
inst✝ : Normal K
hK : K ≤ N
this : Function.Surjective ↑(QuotientGroup.mk' K)
h4 : ¬K = ⊥ ∧ ¬K = N
h5 : Fintype.card (G ⧸ K) < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ map (QuotientGroup.mk' K) N }) (index (map (QuotientGroup.mk' K) N))
H : Subgroup (G ⧸ K)
hH : N ≤ K
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False
exact h4.2 (le_antisymm hK hH)