awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
inst_4 : (↑P : Subgroup G).Normal
K : Subgroup G
hK : K.IsComplement' (↑P : Subgroup G)
h : ⁅K, (↑P : Subgroup G)⁆ = (↑P : Subgroup G)
⊢ ⁅K, (↑P : Subgroup G)⁆ ≤ Bracket.bracket (L := Subgroup G) ⊤ ⊤

Tactic:
exact Subgroup.commutator_mono le_top le_top

Premises used: Subgroup.commutator_mono, le_top
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
⊢ (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal

Tactic:
have : Q.Normal := P.normal_in_normalizer
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
⊢ IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))

Tactic:
have : IsCyclic Q :=
    isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe P.le_normalizer).symm.surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) ∨
    (↑P : Subgroup G) ≤ commutator G

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

Premises used: Sylow.le_center_or_le_commutator, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
refine_1 :
  ∀ (h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ Subgroup.center ↥(Subgroup.normalizer (↑P : Set G))),
    LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
refine_2 :
  ∀ (h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ commutator ↥(Subgroup.normalizer (↑P : Set G))),
    (↑P : Subgroup G) ≤ commutator G
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) ∨
    (↑P : Subgroup G) ≤ commutator G

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

Premises used: Sylow.le_center_or_le_commutator, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ Subgroup.center ↥(Subgroup.normalizer (↑P : Set G))
⊢ Subgroup.normalizer (↑P : Set G) ≤
    Subgroup.map (Subgroup.subtype (Subgroup.normalizer (↑P : Set G)))
      (Subgroup.centralizer
        (↑(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) : Set ↥(Subgroup.normalizer (↑P : Set G))))

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,
      (Subgroup.normalizer (P : Set G)).range_subtype] at h

Premises used: eq_top_iff, MonoidHom.range_eq_map, Subgroup.centralizer_eq_top_iff_subset, Subgroup.map_subtype_le_map_subtype, Subgroup.normalizer, SetLike.coe_subset_coe, SetLike.coe, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h :
  Subgroup.normalizer (↑P : Set G) ≤
    Subgroup.map (Subgroup.subtype (Subgroup.normalizer (↑P : Set G)))
      (Subgroup.centralizer
        (↑(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) : Set ↥(Subgroup.normalizer (↑P : Set G))))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G))
    (Subgroup.centralizer
      ((⇑(Subgroup.subtype (Subgroup.normalizer (↑P : Set G))) : (a : ↥(Subgroup.normalizer (↑P : Set G))) → G) ''
        (↑(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) : Set ↥(Subgroup.normalizer (↑P : Set G)))))

Tactic:
replace h := h.trans (Subgroup.map_centralizer_le_centralizer_image _ _)
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h :
  LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G))
    (Subgroup.centralizer
      ((⇑(Subgroup.subtype (Subgroup.normalizer (↑P : Set G))) : (a : ↥(Subgroup.normalizer (↑P : Set G))) → G) ''
        (↑(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) : Set ↥(Subgroup.normalizer (↑P : Set G)))))
refine_1 :
  ∀
    (h :
      LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G))
        (Subgroup.centralizer
          (↑(Subgroup.map (Subgroup.subtype (Subgroup.normalizer (↑P : Set G)))
                (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))) :
            Set G))),
    LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
refine_1₁ :
  ∀
    (h :
      LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G))
        (Subgroup.centralizer
          (↑(Subgroup.map (G := ↥(Subgroup.normalizer (↑P : Set G)))
                (Subgroup.subtype (Subgroup.normalizer (↑P : Set G)))
                ((↑P : Subgroup G).subgroupOf (Subgroup.normalizer (↑P : Set G)))) :
            Set G))),
    LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
refine_1₂ :
  ∀
    (h :
      LE.le (α := Subgroup G) (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))
        (Subgroup.centralizer
          (↑(Subgroup.map (G := ↥(Subgroup.normalizer (↑(↑P : Subgroup G) : Set G)))
                (Subgroup.subtype (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G)))
                ((↑P : Subgroup G).subgroupOf (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G)))) :
            Set G))),
    LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
refine_1₃ refine_1₄ refine_1₅ refine_1₆ :
  ∀
    (h :
      LE.le (α := Subgroup G) (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))
        (Subgroup.centralizer (↑(↑P : Subgroup G) : Set G))),
    LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))

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

Premises used: Subgroup.coe_map, Subgroup.map_subgroupOf_eq_of_le, Subgroup.le_normalizer, Sylow.coe_coe, Sylow.coe_subtype
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))) ≤ commutator ↥(Subgroup.normalizer (↑P : Set G))
⊢ (↑P : Subgroup G) ≤
    Bracket.bracket (L := Subgroup G) (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))
      (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))

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

Premises used: Subgroup.map_subgroupOf_eq_of_le, Subgroup.map_subtype_le_map_subtype, Subgroup.le_normalizer, Sylow.coe_coe, Sylow.coe_subtype, Subgroup.map_subtype_commutator
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h :
  (↑P : Subgroup G) ≤
    Bracket.bracket (L := Subgroup G) (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))
      (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))
⊢ (↑P : Subgroup G) ≤ commutator G

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

Premises used: Subgroup.commutator_mono, le_top, LE.le.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
Q : Sylow p ↥(Subgroup.normalizer (↑P : Set G)) := P.subtype ⋯
this_1 : (↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G))).Normal
this : IsCyclic.{u_1} ↥(↑Q : Subgroup ↥(Subgroup.normalizer (↑P : Set G)))
h :
  (↑P : Subgroup G) ≤
    Bracket.bracket (L := Subgroup G) (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))
      (Subgroup.normalizer (↑(↑P : Subgroup G) : Set G))
⊢ (↑P : Subgroup G) ≤ commutator G

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

Premises used: Subgroup.commutator_mono, le_top, LE.le.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
⊢ ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)

Tactic:
(normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_

Premises used: Sylow.normalizer_le_centralizer_or_le_commutator, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
refine_1 :
  LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) →
    ¬p ∣ Nat.card.{u_1} ↥(commutator G)
refine_2 : (↑P : Subgroup G) ≤ commutator G → ¬p ∣ Subgroup.index (commutator G)
⊢ ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)

Tactic:
refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_

Premises used: Sylow.normalizer_le_centralizer_or_le_commutator, Or.imp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) →
    ¬p ∣ Nat.card.{u_1} ↥(commutator G)

Tactic:
fun hP h ↦ P.not_dvd_index (h.trans ?_)

Premises used: Sylow.not_dvd_index, Not, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
refine_1 :
  ∀ (hP : LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)))
    (h : p ∣ Nat.card.{u_1} ↥(commutator G)), Nat.card.{u_1} ↥(commutator G) ∣ (↑P : Subgroup G).index
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) →
    ¬p ∣ Nat.card.{u_1} ↥(commutator G)

Tactic:
refine fun hP h ↦ P.not_dvd_index (h.trans ?_)

Premises used: Sylow.not_dvd_index
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
⊢ (↑P : Subgroup G) ≤ commutator G → ¬p ∣ Subgroup.index (commutator G)

Tactic:
fun hP h ↦ P.not_dvd_index (h.trans ?_)

Premises used: Sylow.not_dvd_index, Not, Dvd.dvd.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
refine_2 :
  ∀ (hP : (↑P : Subgroup G) ≤ commutator G) (h : p ∣ Subgroup.index (commutator G)),
    Subgroup.index (commutator G) ∣ (↑P : Subgroup G).index
⊢ (↑P : Subgroup G) ≤ commutator G → ¬p ∣ Subgroup.index (commutator G)

Tactic:
refine fun hP h ↦ P.not_dvd_index (h.trans ?_)

Premises used: Sylow.not_dvd_index
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
hP : LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
h : p ∣ Nat.card.{u_1} ↥(commutator G)
refine_1 : Nat.card.{u_1} ↥(commutator G) ∣ Nat.card.{u_1} ↥(MonoidHom.transferSylow P hP).ker
⊢ Nat.card.{u_1} ↥(commutator G) ∣ (↑P : Subgroup G).index

Tactic:
rw [(MonoidHom.ker_transferSylow_isComplement' P hP).index_eq_card]

Premises used: MonoidHom.ker_transferSylow_isComplement', Subgroup.IsComplement'.index_eq_card
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
hP : LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
h : p ∣ Nat.card.{u_1} ↥(commutator G)
⊢ Nat.card.{u_1} ↥(commutator G) ∣ Nat.card.{u_1} ↥(MonoidHom.transferSylow P hP).ker

Tactic:
Subgroup.card_dvd_of_le (Abelianization.commutator_subset_ker _)

Premises used: Subgroup.card_dvd_of_le, Abelianization.commutator_subset_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
hP : LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
h : p ∣ Nat.card.{u_1} ↥(commutator G)
⊢ Nat.card.{u_1} ↥(commutator G) ∣ Nat.card.{u_1} ↥(MonoidHom.transferSylow P hP).ker

Tactic:
exact Subgroup.card_dvd_of_le (Abelianization.commutator_subset_ker _)

Premises used: Subgroup.card_dvd_of_le, Abelianization.commutator_subset_ker
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
hP : (↑P : Subgroup G) ≤ commutator G
h : p ∣ Subgroup.index (commutator G)
⊢ Subgroup.index (commutator G) ∣ (↑P : Subgroup G).index

Tactic:
Subgroup.index_dvd_of_le hP

Premises used: Subgroup.index_dvd_of_le
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
P : Sylow p G
inst_3 : IsCyclic.{u_1} ↥(↑P : Subgroup G)
hP : (↑P : Subgroup G) ≤ commutator G
h : p ∣ Subgroup.index (commutator G)
⊢ Subgroup.index (commutator G) ∣ (↑P : Subgroup G).index

Tactic:
exact Subgroup.index_dvd_of_le hP

Premises used: Subgroup.index_dvd_of_le
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
h : ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)
contrapose! :
  ∀ (h : (Nat.card.{u_1} ↥(commutator G)).gcd (Subgroup.index (commutator G)) ≠ 1),
    ∃ (p : ℕ), Nat.Prime p ∧ p ∣ Nat.card.{u_1} ↥(commutator G) ∧ p ∣ Subgroup.index (commutator G)
⊢ (Nat.card.{u_1} ↥(commutator G)).Coprime (Subgroup.index (commutator G))

Tactic:
contrapose! h
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
h : (Nat.card.{u_1} ↥(commutator G)).gcd (Subgroup.index (commutator G)) ≠ 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ Nat.card.{u_1} ↥(commutator G) ∧ p ∣ Subgroup.index (commutator G)

Tactic:
Nat.Prime.not_coprime_iff_dvd.mp h

Premises used: Iff.mp, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
h : (Nat.card.{u_1} ↥(commutator G)).gcd (Subgroup.index (commutator G)) ≠ 1
⊢ ∃ (p : ℕ), Nat.Prime p ∧ p ∣ Nat.card.{u_1} ↥(commutator G) ∧ p ∣ Subgroup.index (commutator G)

Tactic:
exact Nat.Prime.not_coprime_iff_dvd.mp h

Premises used: Iff.mp, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
suffices : ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)
⊢ (Nat.card.{u_1} ↥(commutator G)).Coprime (Subgroup.index (commutator G))

Tactic:
suffices h : ∀ p, p.Prime → (¬ p ∣ Nat.card (commutator G) ∨ ¬ p ∣ (commutator G).index) by
    contrapose! h
    exact Nat.Prime.not_coprime_iff_dvd.mp h
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)

Tactic:
Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator default

Premises used: Inhabited.default, Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)

Tactic:
exact Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator default

Premises used: Inhabited.default, Sylow.not_dvd_card_commutator_or_not_dvd_index_commutator
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
h_le : f'.ker ≤ f.range
h_cop : (Nat.card G).Coprime (Nat.card G'')
⊢ IsZGroup G'

Tactic:
⟨fun p hp P ↦ ?_⟩

Premises used: IsZGroup.mk
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
h_le : f'.ker ≤ f.range
h_cop : (Nat.card G).Coprime (Nat.card G'')
refine : ∀ (p : ℕ) (hp : Nat.Prime p) (P : Sylow p G'), IsCyclic.{u_2} ↥(↑P : Subgroup G')
⊢ IsZGroup G'

Tactic:
refine ⟨fun p hp P ↦ ?_⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : 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'
⊢ Fact (Nat.Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : 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)
⊢ (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index

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))
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : 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.{u_2} ↥f'.ker).Coprime f'.ker.index
inl : ∀ (h : (↑P : Subgroup G') ≤ f'.ker), IsCyclic.{u_2} ↥(↑P : Subgroup G')
inr : ∀ (h : Disjoint f'.ker (↑P : Subgroup G')), IsCyclic.{u_2} ↥(↑P : Subgroup G')
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')

Tactic:
rcases P.2.le_or_disjoint_of_coprime h_cop with h | h

Premises used: Sylow.isPGroup', IsPGroup.le_or_disjoint_of_coprime
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : 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.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
⊢ (↑P : Subgroup G') ≤ f.range

Tactic:
replace h_le : P ≤ f.range := h.trans h_le
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
this : IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
have : ∀ (key : ↥((↑P : Subgroup G').subgroupOf f.range) ≃* ↥(↑P : Subgroup G')), IsCyclic.{u_2} ↥(↑P : Subgroup G')
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')

Tactic:
have key := Subgroup.subgroupOfEquivOfLe h_le
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
this : IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
key : ↥((↑P : Subgroup G').subgroupOf f.range) ≃* ↥(↑P : Subgroup G')
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')

Tactic:
isCyclic_of_surjective key key.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective
-- Module: Mathlib.GroupTheory.SpecificGroups.ZGroup
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
f : G →* G'
f' : G' →* G''
inst_3 : Finite G
inst_4 : IsZGroup G
inst_5 : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : (↑P : Subgroup G') ≤ f'.ker
h_le : (↑P : Subgroup G') ≤ f.range
this : IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
key : ↥((↑P : Subgroup G').subgroupOf f.range) ≃* ↥(↑P : Subgroup G')
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')

Tactic:
exact isCyclic_of_surjective key key.surjective

Premises used: isCyclic_of_surjective, MulEquiv.surjective