-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem isZGroup_iff_exists_mulEquiv [Finite G] :
    IsZGroup G ↔ ∃ (N H : Subgroup G) (φ : H →* MulAut N) (_ : G ≃* N ⋊[φ] H),
      IsCyclic H ∧ IsCyclic N ∧ (Nat.card N).Coprime (Nat.card H)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic ↥H
hN : IsCyclic ↥N
hHN : (Nat.card ↥N).Coprime (Nat.card ↥H)
⊢ IsZGroup G

Tactic:
have : IsZGroup (N ⋊[φ] H) :=
  isZGroup_of_coprime SemidirectProduct.range_inl_eq_ker_rightHom.ge hHN

Result:
case refine_2.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic ↥H
hN : IsCyclic ↥N
hHN : (Nat.card ↥N).Coprime (Nat.card ↥H)
this : IsZGroup (↥N ⋊[φ] ↥H)
⊢ IsZGroup G

Proof state:
case refine_1.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Tactic:
have h1 : Abelianization G ≃* H := hH.symm.QuotientMulEquiv

Result:
case refine_1.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
h1 : Abelianization G ≃* ↥H
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Proof state:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ (∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)) → IsZGroup G

Tactic:
rintro ⟨N, H, φ, e, hH, hN, hHN⟩

Result:
case refine_2.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic ↥H
hN : IsCyclic ↥N
hHN : (Nat.card ↥N).Coprime (Nat.card ↥H)
⊢ IsZGroup G

Proof state:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Tactic:
obtain ⟨H, hH⟩ := Subgroup.exists_right_complement'_of_coprime hG.coprime_commutator_index

Result:
case refine_1.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
N H : Subgroup G
φ : ↥H →* MulAut ↥N
e : G ≃* ↥N ⋊[φ] ↥H
hH : IsCyclic ↥H
hN : IsCyclic ↥N
hHN : (Nat.card ↥N).Coprime (Nat.card ↥H)
this : IsZGroup (↥N ⋊[φ] ↥H)
⊢ IsZGroup G

Tactic:
exact IsZGroup.of_injective (f := e.toMonoidHom) e.injective

Result:
no goals

Proof state:
case refine_1.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
h1 : Abelianization G ≃* ↥H
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Tactic:
refine ⟨commutator G, H, _, (SemidirectProduct.mulEquivSubgroup hH).symm,
  isCyclic_of_surjective _ h1.surjective, hG.isCyclic_commutator, ?_⟩

Result:
case refine_1.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
h1 : Abelianization G ≃* ↥H
⊢ (Nat.card ↥(commutator G)).Coprime (Nat.card ↥H)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ IsZGroup G ↔ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

Tactic:
refine ⟨fun hG ↦ ?_, ?_⟩

Result:
case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
⊢ ∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)

case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ (∃ N H φ x, IsCyclic ↥H ∧ IsCyclic ↥N ∧ (Nat.card ↥N).Coprime (Nat.card ↥H)) → IsZGroup G

Proof state:
case refine_1.intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
hG : IsZGroup G
H : Subgroup G
hH : (commutator G).IsComplement' H
h1 : Abelianization G ≃* ↥H
⊢ (Nat.card ↥(commutator G)).Coprime (Nat.card ↥H)

Tactic:
exact Nat.card_congr h1.toEquiv ▸ hG.coprime_commutator_index

Result:
no goals