awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Sylow
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₁ : ℕ
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₂
apply : _root_.Disjoint (↑(P p₁) : Subgroup G) (↑(P p₂) : Subgroup G)
⊢ ∀ (x y : G),
    Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ) G)
        (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₁ hp₁) : ℕ)) x →
      Membership.mem (γ := Sylow (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ) G)
          (P (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ ps) p₂ hp₂) : ℕ)) y →
        Commute x y

Tactic:
apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))

Premises used: Subgroup.commute_of_normal_of_disjoint
-- Module: Mathlib.GroupTheory.Sylow
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₁ : ℕ
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₂
⊢ _root_.Disjoint (↑(P p₁) : Subgroup G) (↑(P p₂) : Subgroup G)

Tactic:
apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'

Premises used: Sylow.isPGroup', IsPGroup.disjoint_of_ne
-- Module: Mathlib.GroupTheory.Sylow
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)
⊢ _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'
-- Module: Mathlib.GroupTheory.Sylow
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 : ℕ)))
refine_2 : ((p : ↥ps) → ↥(P (↑p : ℕ))) ≃* G
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* G

Tactic:
refine MulEquiv.trans (N := ∀ p : ps, P p) ?_ ?_

Premises used: MulEquiv.trans
-- Module: Mathlib.GroupTheory.Sylow
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 : (j : ↥ps) → ((P : Sylow (↑j : ℕ) G) → ↥P) ≃* ↥(↑(P (↑j : ℕ)) : Subgroup G)
⊢ ((p : ↥ps) → (P : Sylow (↑p : ℕ) G) → ↥P) ≃* ((p : ↥ps) → ↥(P (↑p : ℕ)))

Tactic:
apply @MulEquiv.piCongrRight ps (fun p => ∀ P : Sylow p G, P) (fun p => P p) _ _

Premises used: MulEquiv.piCongrRight
-- Module: Mathlib.GroupTheory.Sylow
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
⊢ Fact (Nat.Prime p)

Tactic:
haveI hp' := Fact.mk (Nat.prime_of_mem_primeFactors hp)
-- Module: Mathlib.GroupTheory.Sylow
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_2 : (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
hp' : Fact (Nat.Prime p)
this : Unique (Sylow p G) := (P p).unique_of_normal ⋯
⊢ ((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)

Tactic:
apply MulEquiv.piUnique

Premises used: MulEquiv.piUnique
-- Module: Mathlib.GroupTheory.Sylow
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 :
  Bijective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
    (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)
⊢ ((p : ↥ps) → ↥(P (↑p : ℕ))) ≃* G

Tactic:
apply MulEquiv.ofBijective (Subgroup.noncommPiCoprod hcomm)

Premises used: MulEquiv.ofBijective, Subgroup.noncommPiCoprod
-- Module: Mathlib.GroupTheory.Sylow
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) ∧
    Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card G
⊢ Bijective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
    (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)

Tactic:
apply (Fintype.bijective_iff_injective_and_card _).mpr

Premises used: Iff.mpr, Fintype.bijective_iff_injective_and_card
-- Module: Mathlib.GroupTheory.Sylow
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)
refine_2₁ : Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card 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

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Sylow
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 : iSupIndep.{1, u} (α := Subgroup G) fun (i : ↥ps) ↦ (↑(P (↑i : ℕ)) : Subgroup G)
⊢ Injective (α := (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) (β := G)
    (⇑(noncommPiCoprod hcomm) : (a : (i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) → G)

Tactic:
apply Subgroup.injective_noncommPiCoprod_of_iSupIndep

Premises used: Subgroup.injective_noncommPiCoprod_of_iSupIndep
-- Module: Mathlib.GroupTheory.Sylow
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 :
  _root_.Pairwise fun (i j : ↥ps) ↦
    (Fintype.card.{u} ↥(↑(P (↑i : ℕ)) : Subgroup G)).Coprime (Fintype.card.{u} ↥(↑(P (↑j : ℕ)) : Subgroup G))
⊢ iSupIndep.{1, u} (α := Subgroup G) fun (i : ↥ps) ↦ (↑(P (↑i : ℕ)) : Subgroup G)

Tactic:
apply independent_of_coprime_order hcomm

Premises used: Subgroup.independent_of_coprime_order
-- Module: Mathlib.GroupTheory.Sylow
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₂
⊢ Fact (Nat.Prime p₁)

Tactic:
haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
-- Module: Mathlib.GroupTheory.Sylow
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₁)
⊢ Fact (Nat.Prime p₂)

Tactic:
haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
-- Module: Mathlib.GroupTheory.Sylow
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₂)
⊢ p₁ ≠ p₂

Tactic:
simpa using hne
-- Module: Mathlib.GroupTheory.Sylow
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₂)
⊢ p₁ ≠ p₂

Tactic:
have hne' : p₁ ≠ p₂ := by simpa using hne
-- Module: Mathlib.GroupTheory.Sylow
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₂
refine_2 : (Nat.card.{u} ↥(↑(P p₁) : Subgroup G)).Coprime (Nat.card.{u} ↥(↑(P p₂) : Subgroup G))
⊢ (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))

Tactic:
simp only [← Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Sylow
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₂
⊢ (Nat.card.{u} ↥(↑(P p₁) : Subgroup G)).Coprime (Nat.card.{u} ↥(↑(P p₂) : Subgroup G))

Tactic:
apply IsPGroup.coprime_card_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'

Premises used: Sylow.isPGroup', IsPGroup.coprime_card_of_ne
-- Module: Mathlib.GroupTheory.Sylow
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 : Nat.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Nat.card G
⊢ Fintype.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Fintype.card G

Tactic:
simp only [← Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Sylow
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} ((p : ↥ps) → ↥(P (↑p : ℕ))) = ∏ p : ↥ps, Nat.card.{u} ↥(↑(P (↑p : ℕ)) : Subgroup G)

Tactic:
Nat.card_pi

Premises used: Set.Mem, Nat.card_pi
-- Module: Mathlib.GroupTheory.Sylow
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
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) : ℕ) : ℕ)
⊢ Eq (α := ℕ) (∏ p : ↥ps, Nat.card.{u} ↥(↑(P (↑p : ℕ)) : Subgroup G))
    (∏ p : ↥ps, HPow.hPow (β := ℕ) (↑p : ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))

Tactic:
congr 1 with ⟨p, hp⟩
-- Module: Mathlib.GroupTheory.Sylow
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
⊢ 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:
@card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)

Premises used: Set.Mem, Sylow.card_eq_multiplicity
-- Module: Mathlib.GroupTheory.Sylow
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
⊢ 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:
exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)

Premises used: Sylow.card_eq_multiplicity
-- Module: Mathlib.GroupTheory.Sylow
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, HPow.hPow (β := ℕ) (↑p : ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))
    (∏ p ∈ ps, HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
(Finset.prod_finset_coe (fun p => p ^ (Nat.card G).factorization p) _)

Premises used: Nat.card, HPow.hPow, Finset.prod_finset_coe, DFunLike.coe, Nat.factorization
-- Module: Mathlib.GroupTheory.Sylow
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, HPow.hPow (β := ℕ) p (((Nat.card G).factorization : (a : ℕ) → ℕ) p : ℕ))
    ((Nat.card G).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)

Tactic:
rfl

Premises used: Multiset.toFinset, List.toFinset, Nat.primeFactors, Finsupp.prod, rfl
-- Module: Mathlib.GroupTheory.Sylow
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 G).factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2) = Nat.card G

Tactic:
Nat.prod_factorization_pow_eq_self Nat.card_pos.ne'

Premises used: Nat.card_pos, LT.lt.ne', Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.GroupTheory.Sylow
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 :
  Eq (α := ℕ) (∏ p : ↥ps, Nat.card.{u} ↥(↑(P (↑p : ℕ)) : Subgroup G))
    (∏ p : ↥ps, HPow.hPow (β := ℕ) (↑p : ℕ) (((Nat.card G).factorization : (a : ℕ) → ℕ) (↑p : ℕ) : ℕ))
⊢ Nat.card.{u} ((i : ↥ps) → ↥(↑(P (↑i : ℕ)) : Subgroup G)) = Nat.card G

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'

Premises used: Nat.card_pos, Nat.card, LT.lt.ne', HPow.hPow, Nat.prod_factorization_pow_eq_self, Nat.card_pi, Finset.prod_finset_coe, DFunLike.coe, Nat.factorization, Finsupp.prod, rfl
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
inst : Monoid G
⊢ ¬IsTorsion G ↔ ∃ (g : G), ¬IsOfFinOrder g

Tactic:
not_forall

Premises used: Monoid.IsTorsion, Classical.not_forall
-- Module: Mathlib.GroupTheory.Torsion
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
tG : IsTorsion G
g : G
rw : 1 ≤ orderOf g
⊢ g ^ (orderOf g - 1) * g = 1

Tactic:
rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]

Premises used: pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one