-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem of_surjective [Finite G] [hG : IsZGroup G] (hf : Function.Surjective f) : IsZGroup G'

Proof state:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
⊢ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P

Tactic:
intro p hp P

Result:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
⊢ IsCyclic ↥↑P

Proof state:
case intro
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
Q : Sylow p G
hG : IsCyclic ↥↑Q
⊢ IsCyclic ↥↑(Sylow.mapSurjective hf Q)

Tactic:
exact isCyclic_of_surjective _ (f.subgroupMap_surjective Q)

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : IsZGroup G
hf : Function.Surjective ⇑f
⊢ IsZGroup G'

Tactic:
rw [isZGroup_iff] at hG ⊢

Result:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
⊢ ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P

Proof state:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P

Tactic:
obtain ⟨Q, rfl⟩ := Sylow.mapSurjective_surjective hf p P

Result:
case intro
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
Q : Sylow p G
⊢ IsCyclic ↥↑(Sylow.mapSurjective hf Q)

Proof state:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
⊢ IsCyclic ↥↑P

Tactic:
have := Fact.mk hp

Result:
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P

Proof state:
case intro
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hG : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G), IsCyclic ↥↑P
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
Q : Sylow p G
⊢ IsCyclic ↥↑(Sylow.mapSurjective hf Q)

Tactic:
specialize hG p hp Q

Result:
case intro
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Finite G
hf : Function.Surjective ⇑f
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
Q : Sylow p G
hG : IsCyclic ↥↑Q
⊢ IsCyclic ↥↑(Sylow.mapSurjective hf Q)