-- Mathlib/FieldTheory/Cardinality.lean
theorem Fintype.isPrimePow_card_of_field {α} [Fintype α] [Field α] : IsPrimePow ‖α‖

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
⊢ IsPrimePow ‖α‖

Tactic:
let b := IsNoetherian.finsetBasis (ZMod p) α

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow ‖α‖

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow p

Tactic:
exact hp.1.isPrimePow

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
⊢ IsPrimePow ‖α‖

Tactic:
obtain ⟨p, _⟩ := CharP.exists α

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
⊢ IsPrimePow ‖α‖

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
⊢ IsPrimePow ‖α‖

Tactic:
haveI hp := Fact.mk (CharP.char_is_prime α p)

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
⊢ IsPrimePow ‖α‖

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow ‖α‖

Tactic:
rw [Module.card_fintype b, ZMod.card, isPrimePow_pow_iff]

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow p

case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ ‖{ x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α }‖ ≠ 0

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
⊢ IsPrimePow ‖α‖

Tactic:
letI : Algebra (ZMod p) α := ZMod.algebra _ _

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
⊢ IsPrimePow ‖α‖

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ ‖{ x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α }‖ ≠ 0

Tactic:
rw [← Module.finrank_eq_card_basis b]

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ Module.finrank (ZMod p) α ≠ 0

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ Module.finrank (ZMod p) α ≠ 0

Tactic:
exact Module.finrank_pos.ne'

Result:
no goals