awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)))))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
have 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))
Tactic: rwa [← Subgroup.coe_map, P.coe_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
have 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))
Tactic: rwa [← Subgroup.coe_map, P.coe_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
have 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))
Tactic: rwa [← Subgroup.coe_map, P.coe_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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))
⊢ LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G))
have 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))
Tactic: rwa [← Subgroup.coe_map, P.coe_subtype, ← P.coe_coe,
      Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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) ≤ commutator G
have h₁ : (↑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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
have refine_1 : LE.le (α := Subgroup G) (Subgroup.normalizer (↑P : Set G)) (Subgroup.centralizer (↑P : Set G)) →
  ¬p ∣ Nat.card.{u_1} ↥(commutator G)
Tactic: refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
⊢ ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)
have refine_2 : (↑P : Subgroup G) ≤ commutator G → ¬p ∣ Subgroup.index (commutator G)
Tactic: refine (normalizer_le_centralizer_or_le_commutator P).imp ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
have 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
Tactic: refine fun hP h ↦ P.not_dvd_index (h.trans ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
have refine_2 : ∀ (hP : (↑P : Subgroup G) ≤ commutator G) (h : p ∣ Subgroup.index (commutator G)),
  Subgroup.index (commutator G) ∣ (↑P : Subgroup G).index
Tactic: refine fun hP h ↦ P.not_dvd_index (h.trans ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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) ∣ (↑P : Subgroup G).index
have refine_1 : Nat.card.{u_1} ↥(commutator G) ∣ Nat.card.{u_1} ↥(MonoidHom.transferSylow P hP).ker
Tactic: rw [(MonoidHom.ker_transferSylow_isComplement' P hP).index_eq_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
⊢ (Nat.card.{u_1} ↥(commutator G)).Coprime (Subgroup.index (commutator G))
have 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)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
⊢ (Nat.card.{u_1} ↥(commutator G)).Coprime (Subgroup.index (commutator G))
have suffices : ∀ (p : ℕ), Nat.Prime p → ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ 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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
inst_2 : IsZGroup G
p : ℕ
hp : Nat.Prime p
⊢ ¬p ∣ Nat.card.{u_1} ↥(commutator G) ∨ ¬p ∣ Subgroup.index (commutator G)
have this : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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'
have refine : ∀ (p : ℕ) (hp : Nat.Prime p) (P : Sylow p G'), IsCyclic.{u_2} ↥(↑P : Subgroup G')
Tactic: refine ⟨fun p hp P ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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'
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have this : Fact (Nat.Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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)
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have h_cop₁ : (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))
Cleared hypotheses: h_cop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have inl : ∀ (h : (↑P : Subgroup G') ≤ f'.ker), IsCyclic.{u_2} ↥(↑P : Subgroup G')
Tactic: rcases P.2.le_or_disjoint_of_coprime h_cop with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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')
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have inr : ∀ (h : Disjoint f'.ker (↑P : Subgroup G')), IsCyclic.{u_2} ↥(↑P : Subgroup G')
Tactic: rcases P.2.le_or_disjoint_of_coprime h_cop with h | h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have h_le₁ : (↑P : Subgroup G') ≤ f.range
Tactic: replace h_le : P ≤ f.range := h.trans h_le
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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)
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have have : ∀ (key : ↥((↑P : Subgroup G').subgroupOf f.range) ≃* ↥(↑P : Subgroup G')), IsCyclic.{u_2} ↥(↑P : Subgroup G')
Tactic: have key := Subgroup.subgroupOfEquivOfLe h_le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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 : 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
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have inl : IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
Tactic: suffices IsCyclic (P.subgroupOf f.range) by
      have key := Subgroup.subgroupOfEquivOfLe h_le
      exact isCyclic_of_surjective key key.surjective
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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 : 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
⊢ IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
have inl : ∀ (Q : Sylow p G) (hQ : Sylow.mapSurjective sorry Q = P.subtype h_le),
  IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
Tactic: obtain ⟨Q, hQ⟩ := Sylow.mapSurjective_surjective f.rangeRestrict_surjective p (P.subtype h_le)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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 : 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
Q : Sylow p G
hQ : Sylow.mapSurjective ⋯ Q = P.subtype h_le
⊢ IsCyclic.{u_2} ↥((↑P : Subgroup G').subgroupOf f.range)
have hQ₁ : Subgroup.map f.rangeRestrict (↑Q : Subgroup G) = (↑P : Subgroup G').subgroupOf f.range
Tactic: rw [Sylow.ext_iff, Sylow.coe_mapSurjective, Sylow.coe_subtype] at hQ
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (hypothesis)
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 : Disjoint f'.ker (↑P : Subgroup G')
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have this₁ : IsCyclic.{u_3} ↥(Subgroup.map f' (↑P : Subgroup G'))
Tactic: have := (P.2.map f').isCyclic_of_isZGroup
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker (↑P : Subgroup G')
this : IsCyclic.{u_3} ↥(Subgroup.map f' (↑P : Subgroup G'))
⊢ IsCyclic.{u_2} ↥(↑P : Subgroup G')
have inr : Function.Injective.{u_2 + 1, u_3 + 1} (α := ↥(↑P : Subgroup G')) (β := ↥(Subgroup.map f' (↑P : Subgroup G')))
  (⇑(f'.subgroupMap (↑P : Subgroup G')) : (a : ↥(↑P : Subgroup G')) → ↥(Subgroup.map f' (↑P : Subgroup G')))
Tactic: apply isCyclic_of_injective (f'.subgroupMap P)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker (↑P : Subgroup G')
this : IsCyclic.{u_3} ↥(Subgroup.map f' (↑P : Subgroup G'))
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := ↥(↑P : Subgroup G')) (β := ↥(Subgroup.map f' (↑P : Subgroup G')))
    (⇑(f'.subgroupMap (↑P : Subgroup G')) : (a : ↥(↑P : Subgroup G')) → ↥(Subgroup.map f' (↑P : Subgroup G')))
have inr : Eq (α := Subgroup ↥(↑P : Subgroup G')) (MonoidHom.ker (f'.subgroupMap (↑P : Subgroup G'))) ⊥
Tactic: rwa [← MonoidHom.ker_eq_bot_iff, P.ker_subgroupMap f', Subgroup.subgroupOf_eq_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
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_1 : Fact (Nat.Prime p)
h_cop : (Nat.card.{u_2} ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker (↑P : Subgroup G')
this : IsCyclic.{u_3} ↥(Subgroup.map f' (↑P : Subgroup G'))
inr : Eq (α := Subgroup ↥(↑P : Subgroup G')) (MonoidHom.ker (f'.subgroupMap (↑P : Subgroup G'))) ⊥
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := ↥(↑P : Subgroup G')) (β := ↥(Subgroup.map f' (↑P : Subgroup G')))
    (⇑(f'.subgroupMap (↑P : Subgroup G')) : (a : ↥(↑P : Subgroup G')) → ↥(Subgroup.map f' (↑P : Subgroup G')))
have inr₁ : Eq (α := Subgroup ↥(↑P : Subgroup G')) (f'.ker.subgroupOf (↑P : Subgroup G')) ⊥
Tactic: rwa [← MonoidHom.ker_eq_bot_iff, P.ker_subgroupMap f', Subgroup.subgroupOf_eq_bot]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ IsZGroup G ↔
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
have refine_1 : ∀ (hG : IsZGroup G),
  ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
Tactic: refine ⟨fun hG ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.ZGroup (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
refine_1 :
  ∀ (hG : IsZGroup G),
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
⊢ IsZGroup G ↔
    ∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
      IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)
have refine_2 : (∃ (N : Subgroup G) (H : Subgroup G) (φ : ↥H →* MulAut ↥N) (x : G ≃* ↥N ⋊[φ] ↥H),
    IsCyclic.{u_1} ↥H ∧ IsCyclic.{u_1} ↥N ∧ (Nat.card.{u_1} ↥N).Coprime (Nat.card.{u_1} ↥H)) →
  IsZGroup G
Tactic: refine ⟨fun hG ↦ ?_, ?_⟩