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

Proof state:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
⊢ ∃ H, N.IsComplement' H

Tactic:
refine not_forall_not.mp fun h3 => ?_

Result:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
⊢ False

Proof state:
n : ℕ
⊢ ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
    Nat.card G = n → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H

Tactic:
induction n using Nat.strongRecOn with | ind n ih => ?_

Result:
case ind
n : ℕ
ih :
  ∀ m < n,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
⊢ ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
    Nat.card G = n → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H

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

Tactic:
revert G

Result:
n : ℕ
⊢ ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
    Nat.card G = n → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x✝¹ : Group G'
x✝ : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ Nat.card G' = Nat.card G'

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x✝¹ : Group G'
x✝ : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ ∀ {N' : Subgroup G'} [inst : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'

Tactic:
apply ih _ hG'

Result:
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
G' : Type u
x✝¹ : Group G'
x✝ : Finite G'
hG' : Nat.card G' < Nat.card G
⊢ Nat.card G' = Nat.card G'

Proof state:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
this : N.IsCommutative
⊢ False

Tactic:
exact not_exists_of_forall_not h3 (exists_right_complement'_of_coprime_aux hN)

Result:
no goals

Proof state:
case ind
n : ℕ
ih :
  ∀ m < n,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
⊢ ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
    Nat.card G = n → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H

Tactic:
rintro G _ _ rfl N _ hN

Result:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
⊢ ∃ H, N.IsComplement' H

Proof state:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
⊢ False

Tactic:
haveI := SchurZassenhausInduction.step7 hN (fun G' _ _ hG' => by apply ih _ hG'; rfl) h3

Result:
case ind
G : Type u
inst✝² : Group G
inst✝¹ : Finite G
ih :
  ∀ m < Nat.card G,
    ∀ {G : Type u} [inst : Group G] [inst_1 : Finite G],
      Nat.card G = m → ∀ {N : Subgroup G} [inst_2 : N.Normal], (Nat.card ↥N).Coprime N.index → ∃ H, N.IsComplement' H
N : Subgroup G
inst✝ : N.Normal
hN : (Nat.card ↥N).Coprime N.index
h3 : ∀ (x : Subgroup G), ¬N.IsComplement' x
this : N.IsCommutative
⊢ False