awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
⊢ card.{u_2} (↑(orbit G b) : Type u_2) = 1
have rw₁ : HPow.hPow (β := ℕ) p 0 = 1
Tactic: rw [hk, this, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
⊢ card.{u_2} (↑(orbit G b) : Type u_2) = 1
have rw₂ : Eq (α := ℕ) 1 1
Tactic: rw [hk, this, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ card α ≡ card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have card : ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 = card.{u_2} (↑(fixedPoints G α) : Type u_2)
Tactic: classical
    calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
card : ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 = Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2)
⊢ Fintype.card α ≡ Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have card₁ : ∑ a : Quotient (orbitRel G α), Fintype.card.{u_2} { x : α // Quotient.mk'' x = a } ≡
  ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]
Tactic: classical
    calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
card : ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 = Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2)
card₁ :
  ∑ a : Quotient (orbitRel G α), Fintype.card.{u_2} { x : α // Quotient.mk'' x = a } ≡
    ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]
⊢ Fintype.card α ≡ Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have card₂ : Eq (α := ZMod p) (∑ x : Quotient (orbitRel G α), (↑(Fintype.card.{u_2} { x_1 : α // Quotient.mk'' x_1 = x }) : ZMod p))
  (∑ x : (↑(fixedPoints G α) : Type u_2), (↑1 : ZMod p))
Tactic: classical
    calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
card : ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 = Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2)
card₁ :
  ∑ a : Quotient (orbitRel G α), Fintype.card.{u_2} { x : α // Quotient.mk'' x = a } ≡
    ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]
card₂ :
  Eq (α := ZMod p)
    (∑ x : Quotient (orbitRel G α), (↑(Fintype.card.{u_2} { x_1 : α // Quotient.mk'' x_1 = x }) : ZMod p))
    (∑ x : (↑(fixedPoints G α) : Type u_2), (↑1 : ZMod p))
⊢ Fintype.card α ≡ Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have card₃ : ∀
  (key :
    ∀ (x : α),
      Fintype.card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
        Fintype.card.{u_2} (↑(orbit G x) : Type u_2)),
  Eq (α := ZMod p)
    (∑ x : Quotient (orbitRel G α), (↑(Fintype.card.{u_2} { x_1 : α // Quotient.mk'' x_1 = x }) : ZMod p))
    (∑ x : (↑(fixedPoints G α) : Type u_2), (↑1 : ZMod p))
Tactic: classical
    calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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 α
⊢ Nonempty.{u_3 + 1} (↑(fixedPoints G α) : Type u_3)
have rw : Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) ≠ 0
Tactic: rw [← Finite.card_pos_iff, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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 α
⊢ Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) ≠ 0
have contrapose : ∀ (hpα : Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) = 0), p ∣ Nat.card α
Tactic: contrapose hpα
Cleared hypotheses: hpα
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
⊢ p ∣ Nat.card α
have rw : Nat.card α ≡ Nat.card.{u_3} (↑(fixedPoints G α) : Type u_3) [MOD p]
Tactic: rw [← Nat.modEq_zero_iff_dvd, ← hpα]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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 α
⊢ ∃ b ∈ fixedPoints G α, a ≠ b
have hpf : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b
have hα : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b
have hα₁ : Nontrivial.{u_2} (↑(fixedPoints G α) : Type u_2)
Tactic: rw [Finite.one_lt_card_iff_nontrivial] at hα
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
⊢ 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
Tactic: rw [ConjAct.fixedPoints_eq_center] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
have obtain : ∀ (n : ℕ) (hn0 : n > 0) (hn : Nat.card G = p ^ n), p ∣ Nat.card G
Tactic: obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)
have dvd : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)
have obtain : ∀ (g : G) (hg : g ∈ (↑(Subgroup.center G) : Set G) ∧ 1 ≠ g), Nontrivial.{u_1} ↥(Subgroup.center G)
Tactic: obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
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)
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⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)
have 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)
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⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)
have 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)
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⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ Nontrivial.{u_1} ↥(Subgroup.center G)
have 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)
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⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
⊢ LT.lt (α := Subgroup G) ⊥ (Subgroup.center G)
have this : Nontrivial.{u_1} ↥(Subgroup.center G)
Tactic: haveI := center_nontrivial hG
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ (↑a : G) = (↑b : G)
have change : Eq.{u_1 + 1} (α := G) (↑((Subgroup.inclusion hHK : (a : ↥H) → ↥K) a) : G)
  (↑((Subgroup.inclusion hHK : (a : ↥H) → ↥K) b) : G)
Tactic: change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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 ↥(Subgroup.map ϕ H)
have rw : IsPGroup.{u_2} p ↥(ϕ.comp H.subtype).range
Tactic: rw [← H.range_subtype, MonoidHom.map_range]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ ∃ (k : ℕ), g ^ p ^ k = 1
have obtain : ∀ (j : ℕ)
  (hj : HPow.hPow (α := ↥H) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) ((ϕ : (a : K) → G) (↑g : K)) sorry : ↥H) (p ^ j) = 1),
  ∃ (k : ℕ), g ^ p ^ k = 1
Tactic: obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
⊢ ∃ (k : ℕ), g ^ p ^ k = 1
have hj₁ : 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
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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 : ℕ), g ^ p ^ k = 1
have 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
Tactic: obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
⊢ ∃ (k : ℕ), g ^ p ^ k = 1
have hk₁ : (↑g : K) ^ p ^ (j + k) = (↑1 : K)
Tactic: rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ g ^ p ^ (j + k) = 1
have rwa : (↑(g ^ p ^ (j + k)) : K) = (↑1 : K)
Tactic: rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]