case intro
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
cases nonempty_fintype (fixedPoints G α)
case intro
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
case intro
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
have hpf : p ∣ card (fixedPoints G α) :=
  Nat.modEq_zero_iff_dvd.mp ((hG.card_modEq_card_fixedPoints α).symm.trans hpα.modEq_zero_nat)
case intro
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
hα : 1 < card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
case intro
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
have hα : 1 < card (fixedPoints G α) :=
  (Fact.out (p := p.Prime)).one_lt.trans_le (Nat.le_of_dvd (card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf)
no goals
case intro
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
hα : 1 < card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
exact
  let ⟨⟨b, hb⟩, hba⟩ := exists_ne_of_one_lt_card hα ⟨a, ha⟩
  ⟨b, hb, fun hab => hba (by simp_rw [hab])⟩
no goals
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
hα : 1 < card ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : { val := b, property := hb } ≠ { val := a, property := ha }
hab : a = b
⊢ { val := b, property := hb } = { val := a, property := ha }
simp_rw [hab]