awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
⊢ index (map (QuotientGroup.mk' K) N) = N.index

Tactic:
have index_map := N.index_map_eq this (by rwa [QuotientGroup.ker_mk'])
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
⊢ 0 < N.index

Tactic:
have index_pos : 0 < N.index := Nat.pos_of_ne_zero index_ne_zero_of_finite
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
rw : (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime N.index
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))

Tactic:
rw [index_map]
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime N.index

Tactic:
h1.coprime_dvd_left ?_

Premises used: Nat.Coprime.coprime_dvd_left
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
refine : Nat.card.{u} ↥(map (QuotientGroup.mk' K) N) ∣ Nat.card.{u} ↥N
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime N.index

Tactic:
refine h1.coprime_dvd_left ?_

Premises used: Nat.Coprime.coprime_dvd_left
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
rw : Nat.card.{u} (G ⧸ K) ∣ Nat.card G
⊢ Nat.card.{u} ↥(map (QuotientGroup.mk' K) N) ∣ Nat.card.{u} ↥N

Tactic:
rw [← Nat.mul_dvd_mul_iff_left index_pos, index_mul_card, ← index_map, index_mul_card]

Premises used: Subgroup.index_mul_card, Nat.mul_dvd_mul_iff_left
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
⊢ Nat.card.{u} (G ⧸ K) ∣ Nat.card G

Tactic:
K.card_quotient_dvd_card

Premises used: Subgroup.card_quotient_dvd_card
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
index_map : index (map (QuotientGroup.mk' K) N) = N.index
index_pos : 0 < N.index
⊢ Nat.card.{u} (G ⧸ K) ∣ Nat.card G

Tactic:
exact K.card_quotient_dvd_card

Premises used: Subgroup.card_quotient_dvd_card
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
⊢ (Nat.card.{u} ↥(map (QuotientGroup.mk' K) N)).Coprime (index (map (QuotientGroup.mk' K) N))

Tactic:
have h6 :
    (Nat.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
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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))
obtain :
  ∀ (H : Subgroup (G ⧸ K)) (hH : IsComplement' (map (QuotientGroup.mk' K) N) H), ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤
⊢ ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤

Tactic:
obtain ⟨H, hH⟩ := h2 (G ⧸ K) h5 h6

Premises used: HasQuotient.Quotient
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
⊢ ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤

Tactic:
⟨H.comap (QuotientGroup.mk' K), ?_, ?_⟩

Premises used: QuotientGroup.mk', And.intro, Exists.intro, Subgroup.comap
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
refine_1 : comap (QuotientGroup.mk' K) H ⊔ N = ⊤
refine_2 : comap (QuotientGroup.mk' K) H ≠ ⊤
⊢ ∃ (K : Subgroup G), K ⊔ N = ⊤ ∧ K ≠ ⊤

Tactic:
refine ⟨H.comap (QuotientGroup.mk' K), ?_, ?_⟩
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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) (map (QuotientGroup.mk' K) N) = N

Tactic:
comap_map_eq_self ?_

Premises used: Subgroup.comap_map_eq_self
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
refine : MonoidHom.ker (QuotientGroup.mk' K) ≤ N
⊢ comap (QuotientGroup.mk' K) (map (QuotientGroup.mk' K) N) = N

Tactic:
refine comap_map_eq_self ?_

Premises used: Subgroup.comap_map_eq_self
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
rwa rwa₁ rwa₂ rwa₃ : K ≤ N
⊢ MonoidHom.ker (QuotientGroup.mk' K) ≤ N

Tactic:
rwa [QuotientGroup.ker_mk']

Premises used: QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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) (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']
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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)
refine_1₅ : Eq.{u + 1} (α := Subgroup G) ⊤ ⊤
refine_1₆ : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
refine_1₇ : Eq.{u + 1} (α := Subgroup G) ⊤ ⊤
refine_1₈ refine_1₉ refine_1₁₀ : Function.Surjective (α := G) (β := G ⧸ K) (⇑(QuotientGroup.mk' K) : (a : G) → G ⧸ K)
⊢ comap (QuotientGroup.mk' K) H ⊔ N = ⊤

Tactic:
rwa [← key, comap_sup_eq, hH.symm.sup_eq_top, comap_top]

Premises used: Subgroup.comap_sup_eq, Subgroup.comap_top, Subgroup.IsComplement'.symm, Subgroup.IsComplement'.sup_eq_top
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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) ⊤
⊢ N ≤ K

Tactic:
rw [comap_injective this hH', isComplement'_top_right, map_eq_bot_iff,
      QuotientGroup.ker_mk'] at hH

Premises used: Subgroup.comap_injective, Subgroup.isComplement'_top_right, Subgroup.map_eq_bot_iff, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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) ⊤
hH₁ : N ≤ K
⊢ comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤

Tactic:
rw [comap_injective this hH', isComplement'_top_right, map_eq_bot_iff,
      QuotientGroup.ker_mk'] at hH

Premises used: Subgroup.comap_injective, Subgroup.isComplement'_top_right, Subgroup.map_eq_bot_iff, QuotientGroup.ker_mk'
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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 : N ≤ K
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False

Tactic:
h4.2 (le_antisymm hK hH)

Premises used: le_antisymm, And.right
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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 : N ≤ K
hH' : comap (QuotientGroup.mk' K) H = comap (QuotientGroup.mk' K) ⊤
⊢ False

Tactic:
exact h4.2 (le_antisymm hK hH)

Premises used: le_antisymm, And.right
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
⊢ map N.subtype K = ⊥ ∨ map N.subtype K = N

Tactic:
have key := step2 h1 h2 h3 (K.map N.subtype) (map_subtype_le K)
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
⊢ map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N

Tactic:
rw [← map_bot N.subtype] at key

Premises used: Subgroup.subtype, Subgroup.map_bot
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
rhs : map N.subtype K = N
| map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N

Tactic:
rhs
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
rhs : N
| map N.subtype K = N

Tactic:
rhs
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
rw : map N.subtype ⊤
| N

Tactic:
rw [← N.range_subtype, N.subtype.range_eq_map]

Premises used: Subgroup.subtype, MonoidHom.range_eq_map, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
rw : map N.subtype ⊤
| map N.subtype K = map N.subtype ⊥ ∨ map N.subtype K = N

Tactic:
rhs
    rhs
    rw [← N.range_subtype, N.subtype.range_eq_map]

Premises used: Subgroup.subtype, MonoidHom.range_eq_map, Subgroup.range_subtype