-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem isZGroup_of_coprime [Finite G] [IsZGroup G] [IsZGroup G'']
    (h_le : f'.ker ≤ f.range) (h_cop : (Nat.card G).Coprime (Nat.card G'')) :
    IsZGroup G'

Proof state:
case inr
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ IsCyclic ↥↑P

Tactic:
apply isCyclic_of_injective (f'.subgroupMap P)

Result:
case inr
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ Function.Injective ⇑(f'.subgroupMap ↑P)

Proof state:
case inl.intro
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : ↑P ≤ f'.ker
h_le : ↑P ≤ f.range
Q : Sylow p G
hQ : Sylow.mapSurjective ⋯ Q = P.subtype h_le
⊢ IsCyclic ↥((↑P).subgroupOf f.range)

Tactic:
rw [Sylow.ext_iff, Sylow.coe_mapSurjective, Sylow.coe_subtype] at hQ

Result:
case inl.intro
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : ↑P ≤ f'.ker
h_le : ↑P ≤ f.range
Q : Sylow p G
hQ : Subgroup.map f.rangeRestrict ↑Q = (↑P).subgroupOf f.range
⊢ IsCyclic ↥((↑P).subgroupOf f.range)

Proof state:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : ↑P ≤ f'.ker
h_le : ↑P ≤ f.range
this : IsCyclic ↥((↑P).subgroupOf f.range)
key : ↥((↑P).subgroupOf f.range) ≃* ↥↑P
⊢ IsCyclic ↥↑P

Tactic:
exact isCyclic_of_surjective key key.surjective

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
h_cop : (Nat.card G).Coprime (Nat.card G'')
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P

Tactic:
replace h_cop := (h_cop.of_dvd ((Subgroup.card_dvd_of_le h_le).trans
  (Subgroup.card_range_dvd f)) (Subgroup.index_ker f' ▸ f'.range.card_subgroup_dvd_card))

Result:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
⊢ IsCyclic ↥↑P

Proof state:
case inr
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
⊢ IsCyclic ↥↑P

Tactic:
have := (P.2.map f').isCyclic_of_isZGroup

Result:
case inr
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ IsCyclic ↥↑P