p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
⊢ card (Sylow p G) ≡ 1 [MOD p]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
⊢ card (Sylow p G) ≡ 1 [MOD p]
refine' Sylow.nonempty.elim fun P : Sylow p G => _
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ card (Sylow p G) ≡ 1 [MOD p]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
⊢ card (Sylow p G) ≡ 1 [MOD p]
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
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
⊢ card (Sylow p G) ≡ 1 [MOD p]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ card (Sylow p G) ≡ 1 [MOD p]
have fin : Fintype (fixedPoints P.1 (Sylow p G)) := by
  rw [this]
  infer_instance
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this✝ : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
this : card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) = 1
⊢ card (Sylow p G) ≡ 1 [MOD p]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
⊢ card (Sylow p G) ≡ 1 [MOD p]
have : card (fixedPoints P.1 (Sylow p G)) = 1 := by simp [this]
no goals
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this✝ : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
this : card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) = 1
⊢ card (Sylow p G) ≡ 1 [MOD p]
exact (P.2.card_modEq_card_fixedPoints (Sylow p G)).trans (by rw [this])
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ Fintype ↑{P}
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
rw [this]
no goals
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
⊢ Fintype ↑{P}
infer_instance
no goals
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
⊢ card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) = 1
simp [this]
no goals
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype (Sylow p G)
P : Sylow p G
this✝ : fixedPoints { x // x ∈ ↑P } (Sylow p G) = {P}
fin : Fintype ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G))
this : card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) = 1
⊢ card ↑(fixedPoints { x // x ∈ ↑P } (Sylow p G)) ≡ 1 [MOD p]
rw [this]