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

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

Tactic:
obtain ⟨Q, hQ⟩ := P.exists_comap_eq_of_injective hf

Result:
case intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
⊢ IsCyclic ↥↑P

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑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'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑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'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
hG' : IsCyclic ↥↑Q
h : Subgroup.map f ↑P ≤ ↑Q
⊢ IsCyclic ↥↑P

Tactic:
have := isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe h).surjective

Result:
case intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
hG' : IsCyclic ↥↑Q
h : Subgroup.map f ↑P ≤ ↑Q
this : IsCyclic ↥(Subgroup.map f ↑P)
⊢ IsCyclic ↥↑P

Proof state:
case intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
⊢ IsCyclic ↥↑P

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'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
hG' : IsCyclic ↥↑Q
⊢ IsCyclic ↥↑P

Proof state:
case intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
hG' : IsCyclic ↥↑Q
h : Subgroup.map f ↑P ≤ ↑Q
this : IsCyclic ↥(Subgroup.map f ↑P)
⊢ IsCyclic ↥↑P

Tactic:
exact isCyclic_of_surjective _ (Subgroup.equivMapOfInjective P f hf).symm.surjective

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hG' : IsZGroup G'
hf : Function.Injective ⇑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'
hG' : ∀ (p : ℕ), Nat.Prime p → ∀ (P : Sylow p G'), IsCyclic ↥↑P
hf : Function.Injective ⇑f
⊢ ∀ (p : ℕ), 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'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
hG' : IsCyclic ↥↑Q
⊢ IsCyclic ↥↑P

Tactic:
have h : Subgroup.map f P ≤ Q := hQ ▸ Subgroup.map_comap_le f ↑Q

Result:
case intro
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Injective ⇑f
p : ℕ
hp : Nat.Prime p
P : Sylow p G
Q : Sylow p G'
hQ : Subgroup.comap f ↑Q = ↑P
hG' : IsCyclic ↥↑Q
h : Subgroup.map f ↑P ≤ ↑Q
⊢ IsCyclic ↥↑P