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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ ∃ H, IsComplement' N H
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
hK : K ⊔ N = ⊤
⊢ K = ⊤
contrapose! 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ ∃ H, IsComplement' N H
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ ∃ H, IsComplement' N H
have h4 : (N.comap K.subtype).index = N.index := by
  rw [← N.relindex_top_right, ← hK]
  exact (relindex_sup_right K N).symm
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ ∃ H, IsComplement' N H
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ ∃ H, IsComplement' N H
have h5 : Fintype.card K < Fintype.card G := by
  rw [← K.index_mul_card]
  exact lt_mul_of_one_lt_left Fintype.card_pos (one_lt_index_of_ne_top 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
⊢ ∃ H, IsComplement' N H
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ ∃ H, IsComplement' N H
have h6 : Nat.coprime (Fintype.card (N.comap K.subtype)) (N.comap K.subtype).index := by
  rw [h4]
  exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : IsComplement' (comap (Subgroup.subtype K) N) H
⊢ ∃ H, IsComplement' N H
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
⊢ ∃ H, IsComplement' N H
obtain ⟨H, hH⟩ := h2 K h5 h6
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
⊢ ∃ H, IsComplement' N 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : IsComplement' (comap (Subgroup.subtype K) N) H
⊢ ∃ H, IsComplement' N H
replace hH : Fintype.card (H.map K.subtype) = N.index := by
  rw [←relindex_bot_left_eq_card, ←relindex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
    relindex_bot_left, ←IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
    subtype_range, ←relindex_sup_right, hK, relindex_top_right]
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
⊢ ∃ H, IsComplement' N 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
⊢ ∃ H, IsComplement' N H
have h7 : Fintype.card N * Fintype.card (H.map K.subtype) = Fintype.card G := by
  rw [hH, ← N.index_mul_card, mul_comm]
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
h8 : Nat.coprime (Fintype.card { x // x ∈ N }) (Fintype.card { x // x ∈ map (Subgroup.subtype K) H })
⊢ ∃ H, IsComplement' N 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
⊢ ∃ H, IsComplement' N H
have h8 : (Fintype.card N).coprime (Fintype.card (H.map K.subtype)) := by
  rwa [hH]
no goals
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
h8 : Nat.coprime (Fintype.card { x // x ∈ N }) (Fintype.card { x // x ∈ map (Subgroup.subtype K) H })
⊢ ∃ H, IsComplement' N H
exact ⟨H.map K.subtype, isComplement'_of_coprime h7 h8⟩
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ index (comap (Subgroup.subtype K) N) = relindex N (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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ index (comap (Subgroup.subtype K) N) = index N
rw [← N.relindex_top_right, ← hK]
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ index (comap (Subgroup.subtype K) N) = relindex N (K ⊔ N)
exact (relindex_sup_right K N).symm
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ Fintype.card { x // x ∈ 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ Fintype.card { x // x ∈ K } < Fintype.card G
rw [← 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
⊢ Fintype.card { x // x ∈ K } < index K * Fintype.card { x // x ∈ K }
exact lt_mul_of_one_lt_left Fintype.card_pos (one_lt_index_of_ne_top 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype 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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
rw [h4]
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index N)
exact h1.coprime_dvd_left (card_comap_dvd_of_injective N K.subtype Subtype.coe_injective)
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : IsComplement' (comap (Subgroup.subtype K) N) H
⊢ Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
rw [←relindex_bot_left_eq_card, ←relindex_comap, MonoidHom.comap_bot, Subgroup.ker_subtype,
  relindex_bot_left, ←IsComplement'.index_eq_card (IsComplement'.symm hH), index_comap,
  subtype_range, ←relindex_sup_right, hK, relindex_top_right]
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
⊢ Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
rw [hH, ← N.index_mul_card, mul_comm]
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'
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : index (comap (Subgroup.subtype K) N) = index N
h5 : Fintype.card { x // x ∈ K } < Fintype.card G
h6 : Nat.coprime (Fintype.card { x // x ∈ comap (Subgroup.subtype K) N }) (index (comap (Subgroup.subtype K) N))
H : Subgroup { x // x ∈ K }
hH : Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = index N
h7 : Fintype.card { x // x ∈ N } * Fintype.card { x // x ∈ map (Subgroup.subtype K) H } = Fintype.card G
⊢ Nat.coprime (Fintype.card { x // x ∈ N }) (Fintype.card { x // x ∈ map (Subgroup.subtype K) H })
rwa [hH]