awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
this : Set.Nonempty.{u_1} (α := (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1))
R : (↑(orbit G P) : Type u_1)
hR : Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1)) R
⊢ ∃ (g : G), g • P = (↑R : Sylow p G)

Tactic:
R.2

Premises used: Set.Mem, setOf, MulAction.orbit, Set.range, Subtype.property
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
this : Set.Nonempty.{u_1} (α := (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1))
R : (↑(orbit G P) : Type u_1)
hR : Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1)) R
⊢ ∃ (g : G), g • P = (↑R : Sylow p G)

Tactic:
exact R.2

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
this : Set.Nonempty.{u_1} (α := (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1))
⊢ ∃ (g : G), g • P = Q

Tactic:
exact Exists.elim this fun R hR => by
          rw [← Sylow.ext (H.mp hR)]
          exact R.2

Premises used: Exists.elim
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
suffices :
  Set.Nonempty.{u_1} (α := (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1))
⊢ ∃ (g : G), g • P = Q

Tactic:
suffices Set.Nonempty (fixedPoints Q (orbit G P)) by
        exact Exists.elim this fun R hR => by
          rw [← Sylow.ext (H.mp hR)]
          exact R.2
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
hpα : ¬p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
⊢ Set.Nonempty.{u_1} (α := (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑Q : Subgroup G) (↑(orbit G P) : Type u_1))

Tactic:
apply Q.2.nonempty_fixed_point_of_prime_not_dvd_card

Premises used: Sylow.isPGroup', IsPGroup.nonempty_fixed_point_of_prime_not_dvd_card
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
⊢ ¬p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)

Tactic:
fun h => hp.out.not_dvd_one (Nat.modEq_zero_iff_dvd.mp ?_)

Premises used: Iff.mp, Nat.Prime.not_dvd_one, Nat.modEq_zero_iff_dvd, Not, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
hpα : ∀ (h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)), 1 ≡ 0 [MOD p]
⊢ ¬p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)

Tactic:
refine fun h => hp.out.not_dvd_one (Nat.modEq_zero_iff_dvd.mp ?_)

Premises used: Iff.mp, Nat.Prime.not_dvd_one, Nat.modEq_zero_iff_dvd, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
⊢ 1 = Nat.card.{u_1} (↑(fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) : Type u_1)

Tactic:
?_
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
⊢ Nat.card.{u_1} (↑(fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) : Type u_1) ≡
    Nat.card.{u_1} (↑(orbit G P) : Type u_1) [MOD p]

Tactic:
(P.2.card_modEq_card_fixedPoints (orbit G P)).symm

Premises used: Sylow.isPGroup', Set.Elem, IsPGroup.card_modEq_card_fixedPoints, MulAction.orbit, Nat.ModEq.symm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
⊢ Nat.card.{u_1} (↑(orbit G P) : Type u_1) ≡ 0 [MOD p]

Tactic:
Nat.modEq_zero_iff_dvd.mpr h

Premises used: Iff.mpr, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
hpα : 1 = Nat.card.{u_1} (↑(fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) : Type u_1)
⊢ 1 ≡ 0 [MOD p]

Tactic:
calc
        1 = Nat.card (fixedPoints P (orbit G P)) := ?_
        _ ≡ Nat.card (orbit G P) [MOD p] := (P.2.card_modEq_card_fixedPoints (orbit G P)).symm
        _ ≡ 0 [MOD p] := Nat.modEq_zero_iff_dvd.mpr h

Premises used: Sylow.isPGroup', Sylow.toSubgroup, Iff.mpr, Membership.mem, Set.Elem, Subtype, Nat.card, IsPGroup.card_modEq_card_fixedPoints, MulAction.orbit, Nat.ModEq.symm, MulAction.fixedPoints, Nat.modEq_zero_iff_dvd
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
hpα :
  Nat.card.{u_1} (↑(fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) : Type u_1) =
    Nat.card.{u_1} (↑{Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯} : Type u_1)
⊢ 1 = Nat.card.{u_1} (↑(fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) : Type u_1)

Tactic:
rw [← Nat.card_unique (α := ({⟨P, mem_orbit_self P⟩} : Set (orbit G P))), eq_comm]

Premises used: eq_comm, Nat.card_unique
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
hpα :
  Eq (α := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1))
    {Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯}
⊢ Nat.card.{u_1} (↑(fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) : Type u_1) =
    Nat.card.{u_1} (↑{Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯} : Type u_1)

Tactic:
congr
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
hpα :
  Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1))
      (Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯) ∧
    ∀ (x : (↑(orbit G P) : Type u_1)),
      Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) x →
        x = Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯
⊢ Eq (α := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1))
    {Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯}

Tactic:
rw [Set.eq_singleton_iff_unique_mem]

Premises used: Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
⊢ Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1))
      (Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯) ∧
    ∀ (x : (↑(orbit G P) : Type u_1)),
      Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) x →
        x = Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯

Tactic:
⟨H.mpr rfl, fun R h => Subtype.ext (Sylow.ext (H.mp h))⟩

Premises used: Iff.mpr, Sylow.ext, And.intro, Iff.mp, rfl, Subtype.ext
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
H :
  ∀ {R : Sylow p G} {S : (↑(orbit G P) : Type u_1)},
    Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑R : Subgroup G) (↑(orbit G P) : Type u_1)) S ↔
      (↑(↑S : Sylow p G) : Subgroup G) = (↑R : Subgroup G)
h : p ∣ Nat.card.{u_1} (↑(orbit G P) : Type u_1)
⊢ Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1))
      (Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯) ∧
    ∀ (x : (↑(orbit G P) : Type u_1)),
      Membership.mem (γ := Set (↑(orbit G P) : Type u_1)) (fixedPoints ↥(↑P : Subgroup G) (↑(orbit G P) : Type u_1)) x →
        x = Subtype.mk (p := fun (x : Sylow p G) ↦ x ∈ orbit G P) P ⋯

Tactic:
exact ⟨H.mpr rfl, fun R h => Subtype.ext (Sylow.ext (H.mp h))⟩
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
⊢ Nat.card.{u_1} (Sylow p G) ≡ 1 [MOD p]

Tactic:
Sylow.nonempty.elim fun P : Sylow p G => ?_

Premises used: Nonempty.elim, Sylow.nonempty
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
refine : ∀ (P : Sylow p G), Nat.card.{u_1} (Sylow p G) ≡ 1 [MOD p]
⊢ Nat.card.{u_1} (Sylow p G) ≡ 1 [MOD p]

Tactic:
refine Sylow.nonempty.elim fun P : Sylow p G => ?_

Premises used: Nonempty.elim, Sylow.nonempty
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
⊢ Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}

Tactic:
have : fixedPoints P.1 (Sylow p G) = {P} :=
    Set.ext fun Q : Sylow p G =>
      calc
        Q ∈ fixedPoints P (Sylow p G) ↔ P.1 ≤ Q := P.2.sylow_mem_fixedPoints_iff
        _ ↔ Q.1 = P.1 := ⟨P.3 Q.2, ge_of_eq⟩
        _ ↔ Q ∈ {P} := Sylow.ext_iff.symm.trans Set.mem_singleton_iff.symm
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
this : Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}
⊢ Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) = 1

Tactic:
simp [this]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
this : Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}
⊢ Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) = 1

Tactic:
have : Nat.card (fixedPoints P.1 (Sylow p G)) = 1 := by simp [this]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
this_1 : Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}
this : Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) = 1
rw rw₁ : 1 ≡ 1 [MOD p]
⊢ Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) ≡ 1 [MOD p]

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
this_1 : Eq (α := Set (Sylow p G)) (fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) {P}
this : Nat.card.{u_1} (↑(fixedPoints (↥(↑P : Subgroup G)) (Sylow p G)) : Type u_1) = 1
⊢ Nat.card.{u_1} (Sylow p G) ≡ 1 [MOD p]

Tactic:
exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])

Premises used: Sylow.isPGroup', Sylow, IsPGroup.card_modEq_card_fixedPoints, Nat.ModEq.trans
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
inst_1 : Finite.{u_1 + 1} (Sylow p G)
⊢ ¬p ∣ Nat.card.{u_1} (Sylow p G)

Tactic:
fun h =>
  hp.1.ne_one
    (Nat.dvd_one.mp
      ((Nat.modEq_iff_dvd' zero_le_one).mp
        ((Nat.modEq_zero_iff_dvd.mpr h).symm.trans (card_sylow_modEq_one p G))))

Premises used: Iff.mpr, Nat.dvd_one, Nat.modEq_iff_dvd', zero_le_one, Nat.Prime.ne_one, Nat.ModEq.symm, card_sylow_modEq_one, Iff.mp, Nat.modEq_zero_iff_dvd, Not, Nat.ModEq.trans, Fact.out
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
rw : ↥(↑P : Subgroup G) ≃* ↥(↑(Classical.choose (p := fun (x : G) ↦ x • P = Q) ⋯ • P) : Subgroup G)
⊢ ↥(↑P : Subgroup G) ≃* ↥(↑Q : Subgroup G)

Tactic:
rw [← Classical.choose_spec (exists_smul_eq G P Q)]

Premises used: Classical.choose_spec, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P Q : Sylow p G
⊢ ↥(↑P : Subgroup G) ≃* ↥(↑(Classical.choose (p := fun (x : G) ↦ x • P = Q) ⋯ • P) : Subgroup G)

Tactic:
exact P.equivSMul (Classical.choose (exists_smul_eq G P Q))

Premises used: Sylow.equivSMul, Classical.choose, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
⊢ orbit G P = ⊤

Tactic:
top_le_iff.mp fun Q _ => exists_smul_eq G P Q

Premises used: top_le_iff, Iff.mp, MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
h :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (stabilizer G P) x ↔ Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) x
⊢ Eq (α := Subgroup G) (stabilizer G P) (normalizer (↑P : Set G))

Tactic:
ext
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
P : Sylow p G
x : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G P) x ↔ Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) x

Tactic:
simp [smul_eq_iff_mem_normalizer]

Premises used: Sylow.smul_eq_iff_mem_normalizer
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
rwa : LE.le (α := Subgroup G) (zpowers x) (centralizer (↑(↑P : Subgroup G) : Set G))
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Subgroup G) (centralizer (↑(↑P : Subgroup G) : Set G)) x
⊢ (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)

Tactic:
rwa [le_centralizer_iff, zpowers_le]

Premises used: Subgroup.le_centralizer_iff, Subgroup.zpowers_le
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
⊢ (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)

Tactic:
have h1 : P ≤ centralizer (zpowers x : Set G) := by rwa [le_centralizer_iff, zpowers_le]
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
rw : Membership.mem (γ := Subgroup G) (centralizer (↑(↑(g • P) : Subgroup G) : Set G)) x
⊢ (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)

Tactic:
rw [le_centralizer_iff, zpowers_le]

Premises used: Subgroup.le_centralizer_iff, Subgroup.zpowers_le
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
z : G
hz : z ∈ (↑(↑P : Subgroup G) : Set G)
⊢ z * (g⁻¹ * x * g) = g⁻¹ * x * g * z

Tactic:
specialize hy z hz
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
⊢ (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)

Tactic:
have h2 : ↑(g • P) ≤ centralizer (zpowers x : Set G) := by
    rw [le_centralizer_iff, zpowers_le]
    rintro - ⟨z, hz, rfl⟩
    specialize hy z hz
    rwa [← mul_assoc, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_assoc, mul_assoc, ← mul_assoc,
      eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc] at hy
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h2 : (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
obtain :
  ∀ (h : ↥(centralizer (↑(zpowers x) : Set G))) (hh : h • (g • P).subtype h2 = P.subtype h1),
    ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
obtain ⟨h, hh⟩ :=
    exists_smul_eq (centralizer (zpowers x : Set G)) ((g • P).subtype h2) (P.subtype h1)

Premises used: Subgroup.centralizer, Membership.mem, Subtype, SetLike.coe, Subgroup.zpowers, HSMul.hSMul, MulAction.exists_smul_eq, Sylow.subtype
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h2 : (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h : ↥(centralizer (↑(zpowers x) : Set G))
hh : h • (g • P).subtype h2 = P.subtype h1
⊢ (((↑h : G) * g) • P).subtype ⋯ = P.subtype h1

Tactic:
simp_rw [smul_subtype, Subgroup.smul_def, smul_smul] at hh

Premises used: smul_smul, Subgroup.smul_def, Sylow.smul_subtype
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h2 : (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h : ↥(centralizer (↑(zpowers x) : Set G))
hh : (((↑h : G) * g) • P).subtype ⋯ = P.subtype h1
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
⟨h * g, smul_eq_iff_mem_normalizer.mp (subtype_injective hh), ?_⟩

Premises used: HMul.hMul, Sylow.smul_eq_iff_mem_normalizer, And.intro, Exists.intro, Iff.mp, Sylow.subtype_injective, Subtype.val
-- Module: Mathlib.GroupTheory.Sylow
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite.{u_1 + 1} (Sylow p G)
P : Sylow p G
x g : G
hx : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) x
hy : Membership.mem (γ := Subgroup G) (centralizer (↑P : Set G)) (g⁻¹ * x * g)
h1 : (↑P : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h2 : (↑(g • P) : Subgroup G) ≤ centralizer (↑(zpowers x) : Set G)
h : ↥(centralizer (↑(zpowers x) : Set G))
hh : (((↑h : G) * g) • P).subtype ⋯ = P.subtype h1
refine : g⁻¹ * x * g = ((↑h : G) * g)⁻¹ * x * ((↑h : G) * g)
⊢ ∃ (n : G), Membership.mem (γ := Subgroup G) (normalizer (↑P : Set G)) n ∧ g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
refine ⟨h * g, smul_eq_iff_mem_normalizer.mp (subtype_injective hh), ?_⟩