awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
have hcomm : _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
  ∀ (x y : G),
    Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
      Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
Tactic: have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y := by
    rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
    haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
    haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
    have hne' : p₁ ≠ p₂ := by simpa using hne
    apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))
    apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
have refine_1 : ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* ((p : ↥ps) → ↥(P (↑p : ℕ)))
Tactic: refine MulEquiv.trans (N := ∀ p : ps, P p) ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
refine_1 : ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* ((p : ↥ps) → ↥(P (↑p : ℕ)))
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G
have refine_2 : ((p : ↥ps) → ↥(P (↑p : ℕ))) ≃* G
Tactic: refine MulEquiv.trans (N := ∀ p : ps, P p) ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* ((p : ↥ps) → ↥(P (↑p : ℕ)))
have refine_1 : (j : ↥ps) → ((P : Sylow (↑j : ℕ) G) → ↥P) ≃* ↥(↑(P (↑j : ℕ)) : Subgroup G)
Tactic: apply @MulEquiv.piCongrRight ps (fun p => ∀ P : Sylow p G, P) (fun p => P p) _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
p : ℕ
hp : p ∈ ps
⊢ ((P : Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p hp) : ℕ) G) → ↥P) ≃*
    ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p hp) : ℕ)) : Subgroup G)
have hp' : Fact (Nat.Prime p)
Tactic: haveI hp' := Fact.mk (Nat.prime_of_mem_primeFactors hp)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ ((p : ↥ps) → ↥(P (↑p : ℕ))) ≃* G
have refine_2 : Bijective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
  (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)
Tactic: apply MulEquiv.ofBijective (Subgroup.noncommPiCoprod hcomm)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ Bijective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
    (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)
have refine_2 : Injective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
    (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G) ∧
  Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card G
Tactic: apply (Fintype.bijective_iff_injective_and_card _).mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ Injective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
      (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G) ∧
    Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card G
have refine_2 : Injective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
  (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
refine_2 :
  Injective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
    (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)
⊢ Injective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
      (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G) ∧
    Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card G
have refine_2₁ : Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card G
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ Injective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
    (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)
have refine_2 : iSupIndep.{1, u} (α := Subgroup G) fun (i : ↥ps) ↦ (↑(P (↑i : ℕ)) : Subgroup G)
Tactic: apply Subgroup.injective_noncommPiCoprod_of_iSupIndep
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ iSupIndep.{1, u} (α := Subgroup G) fun (i : ↥ps) ↦ (↑(P (↑i : ℕ)) : Subgroup G)
have refine_2 : _root_.Pairwise fun (i j : ↥ps) ↦
  (Fintype.card.{u} ↥(↑(P (↑i : ℕ)) : Subgroup G)).Coprime (Fintype.card.{u} ↥(↑(P (↑j : ℕ)) : Subgroup G))
Tactic: apply independent_of_coprime_order hcomm
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
⊢ (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) : Subgroup G)).Coprime
    (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) : Subgroup G))
have hp₁' : Fact (Nat.Prime p₁)
Tactic: haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
⊢ (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) : Subgroup G)).Coprime
    (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) : Subgroup G))
have hp₂' : Fact (Nat.Prime p₂)
Tactic: haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (hypothesis)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
⊢ (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) : Subgroup G)).Coprime
    (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) : Subgroup G))
have hne' : p₁ ≠ p₂
Tactic: have hne' : p₁ ≠ p₂ := by simpa using hne
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁ ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) : Subgroup G)).Coprime
    (Fintype.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) : Subgroup G))
have refine_2 : (Nat.card.{u} ↥(↑(P p₁) : Subgroup G)).Coprime (Nat.card.{u} ↥(↑(P p₂) : Subgroup G))
Tactic: simp only [← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card G
have refine_2 : Nat.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Nat.card G
Tactic: simp only [← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ Eq (α := ℕ) (∏ p : ↥ps, Nat.card.{u} ↥(↑(P (↑p : ℕ)) : Subgroup G))
    (∏ p : ↥ps, HPow.hPow (β := ℕ) (↑p : ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))
have e_f : ∀ (p : ℕ) (hp : p ∈ ps),
  Nat.card.{u} ↥(↑(P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p hp) : ℕ)) : Subgroup G) =
    HPow.hPow (β := ℕ) (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p hp) : ℕ)
      (((Nat.card G).factorization : (a : ℕ) → ℕ) (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p hp) : ℕ) : ℕ)
Tactic: congr 1 with ⟨p, hp⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Sylow (goal)
Goal:
G : Type u
inst : Group G
inst_1 : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P : Subgroup G).Normal
this_1 : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥(↑(P p) : Subgroup G)
hcomm :
  _root_.Pairwise fun (p₁ p₂ : ↥ps) ↦
    ∀ (x y : G),
      Membership.mem (γ := Sylow (↑p₁ : ℕ) G) (P (↑p₁ : ℕ)) x →
        Membership.mem (γ := Sylow (↑p₂ : ℕ) G) (P (↑p₂ : ℕ)) y → Commute x y
⊢ Nat.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Nat.card G
have p : Eq (α := ℕ) (∏ p : ↥ps, Nat.card.{u} ↥(↑(P (↑p : ℕ)) : Subgroup G))
  (∏ p : ↥ps, HPow.hPow (β := ℕ) (↑p : ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))
Tactic: calc
      Nat.card (∀ p : ps, P p) = ∏ p : ps, Nat.card (P p) := Nat.card_pi
      _ = ∏ p : ps, p.1 ^ (Nat.card G).factorization p.1 := by
        congr 1 with ⟨p, hp⟩
        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)
      _ = ∏ p ∈ ps, p ^ (Nat.card G).factorization p :=
        (Finset.prod_finset_coe (fun p => p ^ (Nat.card G).factorization p) _)
      _ = (Nat.card G).factorization.prod (· ^ ·) := rfl
      _ = Nat.card G := Nat.prod_factorization_pow_eq_self Nat.card_pos.ne'
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
tG : IsTorsion G
g : G
⊢ g ^ (orderOf g - 1) * g = 1
have rw : 1 ≤ orderOf g
Tactic: rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
f : G →* H
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
tG : IsTorsion G
h : H
⊢ IsOfFinOrder h
have obtain : ∀ (g : G), IsOfFinOrder.{u_2} (G := H) ((f : (a : G) → H) g : H)
Tactic: obtain ⟨g, rfl⟩ := hf h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
⊢ IsOfFinOrder g
have obtain : ∀ (ngn : ℕ) (ngnpos : 0 < ngn) (hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1), IsOfFinOrder g
Tactic: obtain ⟨ngn, ngnpos, hngn⟩ := (tH <| f g).exists_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (hypothesis)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
⊢ IsOfFinOrder g
have hmem : g ^ ngn ∈ f.ker
Tactic: have hmem := MonoidHom.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
hmem : g ^ ngn ∈ f.ker
⊢ IsOfFinOrder g
have lift : ∀ (gn : ↥N) (h : (↑gn : G) = g ^ ngn) (hmem : (↑gn : G) ∈ f.ker), IsOfFinOrder g
Tactic: lift g ^ ngn to N using hN.symm ▸ hmem with gn h
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
⊢ IsOfFinOrder g
have obtain : ∀ (nn : ℕ) (nnpos : 0 < nn) (hnn : gn ^ nn = 1), IsOfFinOrder g
Tactic: obtain ⟨nn, nnpos, hnn⟩ := (tN gn).exists_pow_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
⊢ g ^ (ngn * nn) = 1
have rw : (g ^ ngn) ^ nn = 1
Tactic: rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
rw : (g ^ ngn) ^ nn = 1
⊢ g ^ (ngn * nn) = 1
have rw₁ : (↑gn : G) ^ nn = 1
Tactic: rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
rw : (g ^ ngn) ^ nn = 1
rw₁ : (↑gn : G) ^ nn = 1
⊢ g ^ (ngn * nn) = 1
have rw₂ : (↑(gn ^ nn) : G) = 1
Tactic: rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
rw : (g ^ ngn) ^ nn = 1
rw₁ : (↑gn : G) ^ nn = 1
rw₂ : (↑(gn ^ nn) : G) = 1
⊢ g ^ (ngn * nn) = 1
have rw₃ : Eq.{u_1 + 1} (α := G) (↑1 : G) 1
Tactic: rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
H : Type u_2
inst : Group G
N : Subgroup G
inst_1 : Group H
f : G →* H
hN : N = f.ker
tH : IsTorsion H
tN : IsTorsion.{u_1} ↥N
g : G
ngn : ℕ
ngnpos : 0 < ngn
hngn : HPow.hPow (α := H) ((f : (a : G) → H) g : H) ngn = 1
gn : ↥N
h : (↑gn : G) = g ^ ngn
hmem : (↑gn : G) ∈ f.ker
nn : ℕ
nnpos : 0 < nn
hnn : gn ^ nn = 1
rw : (g ^ ngn) ^ nn = 1
rw₁ : (↑gn : G) ^ nn = 1
rw₂ : (↑(gn ^ nn) : G) = 1
rw₃ : Eq.{u_1 + 1} (α := G) (↑1 : G) 1
⊢ g ^ (ngn * nn) = 1
have rw₄ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : Group G
h : ExponentExists G
g : G
⊢ IsOfFinOrder g
have obtain : ∀ (n : ℕ) (npos : 0 < n) (hn : ∀ (g : G), g ^ n = 1), IsOfFinOrder g
Tactic: obtain ⟨n, npos, hn⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
R : Type u_3
M : Type u_4
inst : AddCommMonoid M
inst_1 : Semiring R
inst_2 : Module R M
tR : IsTorsion R
f : M
⊢ ∃ (n : ℕ), 0 < n ∧ n • f = 0
have obtain : ∀ (n : ℕ) (npos : 0 < n) (hn : HSMul.hSMul (β := R) n 1 = 0), ∃ (n : ℕ), 0 < n ∧ n • f = 0
Tactic: obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : CommMonoid G
x_1 : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun (x_2 : G) ↦ x * x_2) n 1
⊢ Eq.{u_1 + 1} (α := G)
    (↑((fun (x_2 : ↥(torsion G)) ↦
              Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯ * x_2)^[n]
          1) :
      G)
    (↑1 : G)
have dsimp : Eq.{u_1 + 1} (α := G)
  (↑((fun (x_2 : ↥(torsion G)) ↦
            Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x sorry * x_2)^[n]
        1) :
    G)
  1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.GroupTheory.Torsion (goal)
Goal:
G : Type u_1
inst : CommMonoid G
x_1 : ↥(torsion G)
x : G
n : ℕ
npos : n > 0
hn : Function.IsPeriodicPt (fun (x_2 : G) ↦ x * x_2) n 1
⊢ Eq.{u_1 + 1} (α := G)
    (↑((fun (x_2 : ↥(torsion G)) ↦
              Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x ⋯ * x_2)^[n]
          1) :
      G)
    1
have rw : Eq.{u_1 + 1} (α := G)
  (↑((fun (x_2 : ↥(torsion G)) ↦
          HPow.hPow (α := ↥(torsion G))
              (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Submonoid G) (torsion G) x) x sorry) n *
            x_2)
        1) :
    G)
  1
Tactic: rw [mul_left_iterate]