-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem exists_right_complement'_of_coprime {N : Subgroup G} [N.Normal]
    (hN : Nat.Coprime (Nat.card N) N.index) : ∃ H : Subgroup G, IsComplement' N H

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card G ≠ 0

Tactic:
rw [← N.card_mul_index]

Result:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card ↥N * N.index ≠ 0

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card ↥N * N.index ≠ 0

Tactic:
exact mul_ne_zero hN1 hN2

Result:
no goals

Proof state:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
rw [hN2, Nat.coprime_zero_right] at hN

Result:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H

Proof state:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
this : Subsingleton ↥N
⊢ ∃ H, ⊥.IsComplement' H

Tactic:
exact ⟨⊤, isComplement'_bot_top⟩

Result:
no goals

Proof state:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : N = ⊤
hN1 : Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
rw [hN]

Result:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : N = ⊤
hN1 : Nat.card ↥N = 0
⊢ ∃ H, ⊤.IsComplement' H

Proof state:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
rw [hN1, Nat.coprime_zero_left, index_eq_one] at hN

Result:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : N = ⊤
hN1 : Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

Proof state:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : N = ⊤
hN1 : Nat.card ↥N = 0
⊢ ∃ H, ⊤.IsComplement' H

Tactic:
exact ⟨⊥, isComplement'_top_bot⟩

Result:
no goals

Proof state:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
this : Subsingleton ↥N
⊢ ∃ H, N.IsComplement' H

Tactic:
rw [N.eq_bot_of_subsingleton]

Result:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
this : Subsingleton ↥N
⊢ ∃ H, ⊥.IsComplement' H

Proof state:
case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
by_cases hN2 : N.index = 0

Result:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H

case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ ∃ H, N.IsComplement' H

Proof state:
case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
hN3 : Nat.card G ≠ 0
⊢ ∃ H, N.IsComplement' H

Tactic:
haveI := (Cardinal.lt_aleph0_iff_fintype.mp
  (lt_of_not_ge (mt Cardinal.toNat_apply_of_aleph0_le hN3))).some

Result:
case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
hN3 : Nat.card G ≠ 0
this : Fintype G
⊢ ∃ H, N.IsComplement' H

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
⊢ ∃ H, N.IsComplement' H

Tactic:
by_cases hN1 : Nat.card N = 0

Result:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
⊢ ∃ H, N.IsComplement' H

Proof state:
case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
have hN3 : Nat.card G ≠ 0 := by
  rw [← N.card_mul_index]
  exact mul_ne_zero hN1 hN2

Result:
case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
hN3 : Nat.card G ≠ 0
⊢ ∃ H, N.IsComplement' H

Proof state:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
⊢ ∃ H, N.IsComplement' H

Tactic:
haveI := (Cardinal.toNat_eq_one_iff_unique.mp hN).1

Result:
case pos
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : Nat.card ↥N = 1
hN1 : ¬Nat.card ↥N = 0
hN2 : N.index = 0
this : Subsingleton ↥N
⊢ ∃ H, N.IsComplement' H

Proof state:
case neg
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
hN1 : ¬Nat.card ↥N = 0
hN2 : ¬N.index = 0
hN3 : Nat.card G ≠ 0
this : Fintype G
⊢ ∃ H, N.IsComplement' H

Tactic:
exact exists_right_complement'_of_coprime_aux' rfl hN

Result:
no goals