-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem normalizer_le_centralizer_or_le_commutator :
    P.normalizer ≤ Subgroup.centralizer P ∨ P ≤ commutator G

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Tactic:
have : Q.Normal := P.normal_in_normalizer

Result:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this : (↑Q).Normal
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this : (↑Q).Normal
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Tactic:
have : IsCyclic Q :=
  isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe P.le_normalizer).symm.surjective

Result:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Proof state:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : (↑P).normalizer ≤ Subgroup.map (↑P).normalizer.subtype (Subgroup.centralizer ↑↑Q)
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P

Tactic:
replace h := h.trans (Subgroup.map_centralizer_le_centralizer_image _ _)

Result:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : (↑P).normalizer ≤ Subgroup.centralizer (⇑(↑P).normalizer.subtype '' ↑↑Q)
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Tactic:
let Q : Sylow p P.normalizer := P.subtype P.le_normalizer

Result:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Proof state:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : (↑P).normalizer ≤ Subgroup.centralizer (⇑(↑P).normalizer.subtype '' ↑↑Q)
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P

Tactic:
rwa [← Subgroup.coe_map, P.coe_subtype, Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P ∨ ↑P ≤ commutator G

Tactic:
refine (le_center_or_le_commutator Q).imp (fun h ↦ ?_) (fun h ↦ ?_)

Result:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑Q ≤ Subgroup.center ↥(↑P).normalizer
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P

case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑Q ≤ commutator ↥(↑P).normalizer
⊢ ↑P ≤ commutator G

Proof state:
case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑Q ≤ commutator ↥(↑P).normalizer
⊢ ↑P ≤ commutator G

Tactic:
rw [P.coe_subtype, ← Subgroup.map_subtype_le_map_subtype,
  Subgroup.map_subgroupOf_eq_of_le P.le_normalizer, Subgroup.map_subtype_commutator] at h

Result:
case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑P ≤ ⁅(↑P).normalizer, (↑P).normalizer⁆
⊢ ↑P ≤ commutator G

Proof state:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑Q ≤ Subgroup.center ↥(↑P).normalizer
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P

Tactic:
rw [← SetLike.coe_subset_coe, ← Subgroup.centralizer_eq_top_iff_subset, eq_top_iff,
  ← Subgroup.map_subtype_le_map_subtype, ← MonoidHom.range_eq_map,
  P.normalizer.range_subtype] at h

Result:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : (↑P).normalizer ≤ Subgroup.map (↑P).normalizer.subtype (Subgroup.centralizer ↑↑Q)
⊢ (↑P).normalizer ≤ Subgroup.centralizer ↑P

Proof state:
case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(↑P).normalizer := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑P ≤ ⁅(↑P).normalizer, (↑P).normalizer⁆
⊢ ↑P ≤ commutator G

Tactic:
exact h.trans (Subgroup.commutator_mono le_top le_top)

Result:
no goals