awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
this_1 : Fintype α
this : Fintype (↑(fixedPoints G α) : Type u_2)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
b_1 : Quotient (orbitRel G α)
b : α
h : Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b)
hb :
  Ne (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
k : ℕ
hk : Nat.card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
⊢ card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k

Tactic:
rw [Nat.card_eq_fintype_card] at hk

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
this_1 : Fintype α
this : Fintype (↑(fixedPoints G α) : Type u_2)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
b_1 : Quotient (orbitRel G α)
b : α
h : Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b)
hb :
  Ne (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
k : ℕ
hk : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
contrapose! :
  ∀ (hb : k ≠ 0),
    Eq (α := ZMod p)
      (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
⊢ k = 0

Tactic:
contrapose! hb
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
this_1 : Fintype α
this : Fintype (↑(fixedPoints G α) : Type u_2)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
b_1 : Quotient (orbitRel G α)
b : α
h : Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b)
k : ℕ
hk : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
hb : k ≠ 0
⊢ Eq (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0

Tactic:
simp [key, hk, hb]
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
this_1 : Fintype α
this : Fintype (↑(fixedPoints G α) : Type u_2)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
b_1 : Quotient (orbitRel G α)
b : α
h : Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b)
hb :
  Ne (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
k : ℕ
hk : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
⊢ k = 0

Tactic:
have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
this_1 : Fintype α
this_2 : Fintype (↑(fixedPoints G α) : Type u_2)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
b_1 : Quotient (orbitRel G α)
b : α
h : Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b)
hb :
  Ne (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
k : ℕ
hk : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
this : k = 0
rw : p ^ k = 1
rw₁ : HPow.hPow (β := ℕ) p 0 = 1
rw₂ rw₃ : Eq (α := ℕ) 1 1
⊢ card.{u_2} (↑(orbit G b) : Type u_2) = 1

Tactic:
rw [hk, this, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
this_1 : Fintype α
this_2 : Fintype (↑(fixedPoints G α) : Type u_2)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
b_1 : Quotient (orbitRel G α)
b : α
h : Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b)
hb :
  Ne (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
k : ℕ
hk : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
this : k = 0
⊢ ∃ (a : (↑(fixedPoints G α) : Type u_2)) (h₁ :
    Membership.mem (γ := Finset (↑(fixedPoints G α) : Type u_2)) Finset.univ a) (h₂ : Ne (α := ZMod p) (↑1 : ZMod p) 0),
    Eq (α := Quotient (orbitRel G α))
      ((fun (a : (↑(fixedPoints G α) : Type u_2))
            (x : Membership.mem (γ := Finset (↑(fixedPoints G α) : Type u_2)) Finset.univ a)
            (x_1 : Ne (α := ZMod p) (↑1 : ZMod p) 0) ↦
          (Quotient.mk'' (↑a : α) : Quotient (orbitRel G α)))
        a h₁ h₂)
      (Quotient.mk'' b)

Tactic:
exact
      ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩,
        Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst_1 : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
rw : Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) ≠ 0
⊢ Nonempty.{u_3 + 1} (↑(fixedPoints G α) : Type u_3)

Tactic:
rw [← Finite.card_pos_iff, pos_iff_ne_zero]

Premises used: Finite.card_pos_iff, pos_iff_ne_zero
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst_1 : MulAction G α
hpα : ¬p ∣ Nat.card α
this : Finite α
contrapose : ∀ (hpα : Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) = 0), p ∣ Nat.card α
⊢ Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) ≠ 0

Tactic:
contrapose hpα
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst_1 : MulAction G α
this : Finite α
hpα : Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) = 0
rw : Nat.card α ≡ Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) [MOD p]
⊢ p ∣ Nat.card α

Tactic:
rw [← Nat.modEq_zero_iff_dvd, ← hpα]

Premises used: Nat.modEq_zero_iff_dvd
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst_1 : MulAction G α
this : Finite α
hpα : Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) = 0
⊢ Nat.card α ≡ Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) [MOD p]

Tactic:
hG.card_modEq_card_fixedPoints α

Premises used: IsPGroup.card_modEq_card_fixedPoints
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_3
inst_1 : MulAction G α
this : Finite α
hpα : Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) = 0
⊢ Nat.card α ≡ Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) [MOD p]

Tactic:
exact hG.card_modEq_card_fixedPoints α

Premises used: IsPGroup.card_modEq_card_fixedPoints
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
⊢ p ∣ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2)

Tactic:
have hpf : p ∣ Nat.card (fixedPoints G α) :=
    Nat.modEq_zero_iff_dvd.mp ((hG.card_modEq_card_fixedPoints α).symm.trans hpα.modEq_zero_nat)
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2)
⊢ 1 < Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2)

Tactic:
have hα : 1 < Nat.card (fixedPoints G α) :=
    (Fact.out (p := p.Prime)).one_lt.trans_le (Nat.le_of_dvd (Finite.card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf)
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2)
hα : 1 < Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2)
⊢ Nontrivial.{u_2} (↑(fixedPoints G α) : Type u_2)

Tactic:
rw [Finite.one_lt_card_iff_nontrivial] at hα

Premises used: Finite.one_lt_card_iff_nontrivial
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2)
hα : Nontrivial.{u_2} (↑(fixedPoints G α) : Type u_2)
b : α
hb : b ∈ fixedPoints G α
hba :
  Subtype.mk (p := fun (x : α) ↦ x ∈ fixedPoints G α) b hb ≠ Subtype.mk (p := fun (x : α) ↦ x ∈ fixedPoints G α) a ha
hab : a = b
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ fixedPoints G α) b hb = Subtype.mk (p := fun (x : α) ↦ x ∈ fixedPoints G α) a ha

Tactic:
simp_rw [hab]
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2)
hα : Nontrivial.{u_2} (↑(fixedPoints G α) : Type u_2)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
exact
    let ⟨⟨b, hb⟩, hba⟩ := exists_ne (⟨a, ha⟩ : fixedPoints G α)
    ⟨b, hb, fun hab => hba (by simp_rw [hab])⟩
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
⊢ ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ fixedPoints (ConjAct G) G), ∃ b ∈ fixedPoints (ConjAct G) G, a ≠ b

Tactic:
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this : ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ fixedPoints (ConjAct G) G), ∃ b ∈ fixedPoints (ConjAct G) G, a ≠ b
⊢ ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b

Tactic:
rw [ConjAct.fixedPoints_eq_center] at this

Premises used: ConjAct.fixedPoints_eq_center
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this :
  ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b
obtain : ∀ (n : ℕ) (hn0 : n > 0) (hn : Nat.card G = p ^ n), p ∣ Nat.card G
⊢ p ∣ Nat.card G

Tactic:
obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance

Premises used: inferInstance, IsPGroup.nontrivial_iff_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this :
  ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b
n : ℕ
hn0 : n > 0
hn : Nat.card G = p ^ n
⊢ p ∣ Nat.card G

Tactic:
hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)

Premises used: Eq.rec, ne_of_gt, dvd_pow_self, Eq.symm
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this :
  ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b
n : ℕ
hn0 : n > 0
hn : Nat.card G = p ^ n
⊢ p ∣ Nat.card G

Tactic:
exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this :
  ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b
⊢ p ∣ Nat.card G

Tactic:
have dvd : p ∣ Nat.card G := by
      obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
      exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this :
  ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b
dvd : p ∣ Nat.card G
obtain : ∀ (g : G) (hg : g ∈ (↑(Subgroup.center G) : Set G) ∧ 1 ≠ g), Nontrivial.{u_1} ↥(Subgroup.center G)
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)

Tactic:
obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem

Premises used: Subgroup.center, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this :
  ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b
dvd : p ∣ Nat.card G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G) ∧ 1 ≠ g
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)

Tactic:
⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩

Premises used: mt, Nontrivial.mk, Subtype.ext_iff, Subtype.mk, And.right, And.left, Exists.intro, Iff.mp, OfNat.ofNat
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this :
  ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
    ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b
dvd : p ∣ Nat.card G
g : G
hg : g ∈ (↑(Subgroup.center G) : Set G) ∧ 1 ≠ g
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)

Tactic:
exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
have have₁ have₂ :
  ∀
    (this :
      ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ fixedPoints (ConjAct G) G), ∃ b ∈ fixedPoints (ConjAct G) G, a ≠ b),
    Nontrivial.{u_1} ↥(Subgroup.center G)
have₃ :
  ∀
    (this :
      ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
        ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b),
    Nontrivial.{u_1} ↥(Subgroup.center G)
have₄ :
  ∀
    (this :
      ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
        ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b)
    (dvd : p ∣ Nat.card G), Nontrivial.{u_1} ↥(Subgroup.center G)
have₅ :
  ∀
    (this :
      ∀ (hpα : p ∣ Nat.card G) {a : G} (ha : a ∈ (↑(Subgroup.center G) : Set G)),
        ∃ b ∈ (↑(Subgroup.center G) : Set G), a ≠ b)
    (dvd : p ∣ Nat.card G) (g : G) (hg : g ∈ (↑(Subgroup.center G) : Set G) ∧ 1 ≠ g),
    Nontrivial.{u_1} ↥(Subgroup.center G)
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)

Tactic:
classical
    have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
    rw [ConjAct.fixedPoints_eq_center] at this
    have dvd : p ∣ Nat.card G := by
      obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
      exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
    obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
    exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩

Premises used: ConjAct.fixedPoints_eq_center
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)

Tactic:
haveI := center_nontrivial hG
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this : Nontrivial.{u_1} ↥(Subgroup.center G)
⊢ LT.lt (α := Subgroup G) ⊥ (Subgroup.center G)

Tactic:
bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

Premises used: Iff.mpr, Subgroup.one_lt_card_iff_ne_bot, bot_lt_iff_ne_bot, Subgroup.center, Finite.one_lt_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this : Nontrivial.{u_1} ↥(Subgroup.center G)
⊢ LT.lt (α := Subgroup G) ⊥ (Subgroup.center G)

Tactic:
exact
      bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

Premises used: Iff.mpr, Subgroup.one_lt_card_iff_ne_bot, bot_lt_iff_ne_bot, Subgroup.center, Finite.one_lt_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Nontrivial G
inst_2 : Finite G
this : Nontrivial.{u_1} ↥(Subgroup.center G)
⊢ LT.lt (α := Subgroup G) ⊥ (Subgroup.center G)

Tactic:
classical exact
      bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Finite.one_lt_card)

Premises used: Iff.mpr, Subgroup.one_lt_card_iff_ne_bot, bot_lt_iff_ne_bot, Subgroup.center, Finite.one_lt_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H K : Subgroup G
hK : IsPGroup.{u_1} p ↥K
hHK : H ≤ K
a b : ↥H
h : Eq (α := ↥K) ((Subgroup.inclusion hHK : (a : ↥H) → ↥K) a : ↥K) ((Subgroup.inclusion hHK : (a : ↥H) → ↥K) b : ↥K)
change :
  Eq.{u_1 + 1} (α := G) (↑((Subgroup.inclusion hHK : (a : ↥H) → ↥K) a) : G)
    (↑((Subgroup.inclusion hHK : (a : ↥H) → ↥K) b) : G)
⊢ (↑a : G) = (↑b : G)

Tactic:
change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b

Premises used: Subgroup.inclusion, Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H K : Subgroup G
hK : IsPGroup.{u_1} p ↥K
hHK : H ≤ K
a b : ↥H
h : Eq (α := ↥K) ((Subgroup.inclusion hHK : (a : ↥H) → ↥K) a : ↥K) ((Subgroup.inclusion hHK : (a : ↥H) → ↥K) b : ↥K)
⊢ Eq.{u_1 + 1} (α := G) (↑((Subgroup.inclusion hHK : (a : ↥H) → ↥K) a) : G)
    (↑((Subgroup.inclusion hHK : (a : ↥H) → ↥K) b) : G)

Tactic:
apply Subtype.ext_iff.mp h

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H K : Subgroup G
hH : IsPGroup.{u_1} p ↥H
⊢ IsPGroup.{u_1} p ↥(H ⊓ K)

Tactic:
hH.to_le inf_le_left

Premises used: IsPGroup.to_le, inf_le_left
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H K : Subgroup G
hK : IsPGroup.{u_1} p ↥K
⊢ IsPGroup.{u_1} p ↥(H ⊓ K)

Tactic:
hK.to_le inf_le_right

Premises used: inf_le_right, IsPGroup.to_le
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : G →* K
rw : IsPGroup.{u_2} p ↥(ϕ.comp H.subtype).range
⊢ IsPGroup.{u_2} p ↥(Subgroup.map ϕ H)

Tactic:
rw [← H.range_subtype, MonoidHom.map_range]

Premises used: MonoidHom.map_range, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : G →* K
⊢ IsPGroup.{u_2} p ↥(ϕ.comp H.subtype).range

Tactic:
hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective

Premises used: IsPGroup.of_surjective, MonoidHom.rangeRestrict, MonoidHom.restrict, MonoidHom.rangeRestrict_surjective
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : G →* K
⊢ IsPGroup.{u_2} p ↥(ϕ.comp H.subtype).range

Tactic:
exact hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective

Premises used: IsPGroup.of_surjective, MonoidHom.rangeRestrict, MonoidHom.restrict, MonoidHom.rangeRestrict_surjective
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
obtain :
  ∀ (j : ℕ)
    (hj : HPow.hPow (α := ↥H) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((ϕ : (a : K) → G) (↑g : K)) ⋯ : ↥H) (p ^ j) = 1),
    ∃ (k : ℕ), g ^ p ^ k = 1
⊢ ∃ (k : ℕ), g ^ p ^ k = 1

Tactic:
obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩

Premises used: Subtype.mk, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : HPow.hPow (α := ↥H) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((ϕ : (a : K) → G) (↑g : K)) ⋯ : ↥H) (p ^ j) = 1
⊢ Eq.{u_1 + 1} (α := G) ((ϕ : (a : K) → G) ((↑g : K) ^ p ^ j) : G) ((↑1 : G) : G)

Tactic:
rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj

Premises used: Subtype.coe_mk, Subgroup.coe_pow, Subtype.ext_iff, MonoidHom.map_pow
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : Eq.{u_1 + 1} (α := G) ((ϕ : (a : K) → G) ((↑g : K) ^ p ^ j) : G) ((↑1 : G) : G)
obtain :
  ∀ (k : ℕ)
    (hk : HPow.hPow (α := ↥ϕ.ker) (Subtype.mk (p := fun (x : K) ↦ x ∈ ϕ.ker) ((↑g : K) ^ p ^ j) hj) (p ^ k) = 1),
    ∃ (k : ℕ), g ^ p ^ k = 1
⊢ ∃ (k : ℕ), g ^ p ^ k = 1

Tactic:
obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩

Premises used: Subtype.mk, HPow.hPow, Subtype.val
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : Eq.{u_1 + 1} (α := G) ((ϕ : (a : K) → G) ((↑g : K) ^ p ^ j) : G) ((↑1 : G) : G)
k : ℕ
hk : HPow.hPow (α := ↥ϕ.ker) (Subtype.mk (p := fun (x : K) ↦ x ∈ ϕ.ker) ((↑g : K) ^ p ^ j) hj) (p ^ k) = 1
⊢ (↑g : K) ^ p ^ (j + k) = (↑1 : K)

Tactic:
rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk

Premises used: Subtype.coe_mk, pow_add, Subgroup.coe_pow, pow_mul, Subtype.ext_iff, MonoidHom.ker
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : Eq.{u_1 + 1} (α := G) ((ϕ : (a : K) → G) ((↑g : K) ^ p ^ j) : G) ((↑1 : G) : G)
k : ℕ
hk : (↑g : K) ^ p ^ (j + k) = (↑1 : K)
rwa : (↑(g ^ p ^ (j + k)) : K) = (↑1 : K)
rwa₁ rwa₂ rwa₃ rwa₄ : (↑g : K) ^ p ^ (j + k) = (↑1 : K)
⊢ g ^ p ^ (j + k) = 1

Tactic:
rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]

Premises used: Subgroup.coe_pow, Subtype.ext_iff, Subgroup.comap
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
H : Subgroup G
hH : IsPGroup.{u_1} p ↥H
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : IsPGroup.{u_2} p ↥ϕ.ker
g : ↥(Subgroup.comap ϕ H)
j : ℕ
hj : Eq.{u_1 + 1} (α := G) ((ϕ : (a : K) → G) ((↑g : K) ^ p ^ j) : G) ((↑1 : G) : G)
k : ℕ
hk : (↑g : K) ^ p ^ (j + k) = (↑1 : K)
⊢ ∃ (k : ℕ), g ^ p ^ k = 1

Tactic:
exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
K : Type u_2
inst_1 : Group K
ϕ : K →* G
hϕ : Function.Injective.{u_2 + 1, u_1 + 1} (α := K) (β := G) (⇑ϕ : (a : K) → G)
⊢ IsPGroup.{u_2} p ↥ϕ.ker

Tactic:
(congr_arg (fun Q : Subgroup K => IsPGroup p Q) (ϕ.ker_eq_bot_iff.mpr hϕ)).mpr IsPGroup.of_bot

Premises used: Iff.mpr, Eq.mpr, IsPGroup, Membership.mem, Subtype, congr_arg, MonoidHom.ker_eq_bot_iff, IsPGroup.of_bot