-- Mathlib/FieldTheory/Finite/Basic.lean
theorem card (p : ℕ) [CharP K p] : ∃ n : ℕ+, Nat.Prime p ∧ q = p ^ (n : ℕ)

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = p ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
refine ⟨⟨n, ?_⟩, hp.1, h⟩

Result:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = p ^ n
⊢ 0 < n

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this✝ : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
h : q = 1
this : 0 = 1
⊢ False

Tactic:
exact absurd this zero_ne_one

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
h : q = p ^ 0
⊢ False

Tactic:
rw [pow_zero] at h

Result:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
h : q = 1
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime K p⟩

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
h : q = 1
⊢ False

Tactic:
have : (0 : K) = 1 := by apply Fintype.card_le_one_iff.mp (le_of_eq h)

Result:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this✝ : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
h : q = 1
this : 0 = 1
⊢ False

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = p ^ n
⊢ ¬n = 0

Tactic:
rintro rfl

Result:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
h : q = p ^ 0
⊢ False

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
h : q = 1
⊢ 0 = 1

Tactic:
apply Fintype.card_le_one_iff.mp (le_of_eq h)

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
rw [ZMod.card] at h

Result:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = p ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
obtain ⟨n, h⟩ := VectorSpace.card_fintype (ZMod p) K

Result:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = Fintype.card (ZMod p) ^ n
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Proof state:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = p ^ n
⊢ 0 < n

Tactic:
apply Or.resolve_left (Nat.eq_zero_or_pos n)

Result:
case intro
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
n : ℕ
h : q = p ^ n
⊢ ¬n = 0

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n

Tactic:
letI : Module (ZMod p) K := { (ZMod.castHom dvd_rfl K : ZMod p →+* _).toModule with }

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p : ℕ
inst✝ : CharP K p
hp : Fact (Nat.Prime p)
this : Module (ZMod p) K :=
  let __src := (ZMod.castHom ⋯ K).toModule;
  Module.mk ⋯ ⋯
⊢ ∃ n, Nat.Prime p ∧ q = p ^ ↑n