-- Mathlib/FieldTheory/Finite/GaloisField.lean
theorem finrank {n} (h : n ≠ 0) : Module.finrank (ZMod p) (GaloisField p n) = n

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this✝ : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
nat_degree_eq : g_poly.natDegree = p ^ n
this : g_poly.rootSet (GaloisField p n) = Set.univ
key : Fintype.card (GaloisField p n) = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
rw [@card_eq_pow_finrank (ZMod p) _ _ _ _ _ (_), ZMod.card] at key

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this✝ : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
nat_degree_eq : g_poly.natDegree = p ^ n
this : g_poly.rootSet (GaloisField p n) = Set.univ
key : p ^ Module.finrank (ZMod p) (GaloisField p n) = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
suffices g_poly.rootSet (GaloisField p n) = Set.univ by
  simp_rw [this, ← Fintype.ofEquiv_card (Equiv.Set.univ _)] at key
  rw [@card_eq_pow_finrank (ZMod p) _ _ _ _ _ (_), ZMod.card] at key
  exact Nat.pow_right_injective (Nat.Prime.one_lt' p).out key

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
⊢ g_poly.rootSet (GaloisField p n) = Set.univ

Proof state:
case succ.refine_2
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ((X ^ (n✝ + 1) ^ n - X).coeff 0) = 0

Tactic:
simp only [g_poly, coeff_X_pow, coeff_X_zero, sub_zero, _root_.map_eq_zero, ite_eq_right_iff,
  one_ne_zero, coeff_sub]

Result:
case succ.refine_2
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ 0 = (n✝ + 1) ^ n → False

Proof state:
case zero
n : ℕ
h : n ≠ 0
h_prime : Fact (Nat.Prime 0)
this : Fintype (GaloisField 0 n)
g_poly : (ZMod 0)[X] := X ^ 0 ^ n - X
hp : 1 < 0
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField 0 n)) = 0 ^ n
nat_degree_eq : g_poly.natDegree = 0 ^ n
x : GaloisField 0 n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod 0) (GaloisField 0 n)) ∪ (X ^ 0 ^ n - X).rootSet (X ^ 0 ^ n - X).SplittingField)
⊢ x ∈ (X ^ 0 ^ n - X).rootSet (GaloisField 0 n)

case succ
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Tactic:
cases hp

Result:
case succ
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
⊢ x ∈ (X ^ (n✝ + 1) ^ n - X).rootSet (GaloisField (n✝ + 1) n)

Proof state:
case succ.refine_1.inl.intro
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
r : ZMod (n✝ + 1)
⊢ (aeval ((algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r)) (X ^ (n✝ + 1) ^ n - X) = 0

Tactic:
simp only [g_poly, map_sub, map_pow, aeval_X]

Result:
case succ.refine_1.inl.intro
n : ℕ
h : n ≠ 0
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
this : Fintype (GaloisField (n✝ + 1) n)
g_poly : (ZMod (n✝ + 1))[X] := X ^ (n✝ + 1) ^ n - X
hp : 1 < n✝ + 1
aux : X ^ (n✝ + 1) ^ n - X ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField (n✝ + 1) n)) = (n✝ + 1) ^ n
nat_degree_eq : g_poly.natDegree = (n✝ + 1) ^ n
x : GaloisField (n✝ + 1) n
hx :
  x ∈
    Subring.closure
      (Set.range ⇑(algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) ∪
        (X ^ (n✝ + 1) ^ n - X).rootSet (X ^ (n✝ + 1) ^ n - X).SplittingField)
r : ZMod (n✝ + 1)
⊢ (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r ^ (n✝ + 1) ^ n -
      (algebraMap (ZMod (n✝ + 1)) (GaloisField (n✝ + 1) n)) r =
    0

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this✝ : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
aux : g_poly ≠ 0
key : Fintype.card ↑(g_poly.rootSet (GaloisField p n)) = p ^ n
nat_degree_eq : g_poly.natDegree = p ^ n
this : ∀ x ∈ ⊤, x ∈ (X ^ p ^ n - X).rootSet (GaloisField p n)
⊢ ∀ (x : GaloisField p n), x ∈ g_poly.rootSet (GaloisField p n)

Tactic:
simpa

Result:
no goals

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
⊢ Module.finrank (ZMod p) (GaloisField p n) = n

Tactic:
have hp : 1 < p := h_prime.out.one_lt

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
this : Fintype (GaloisField p n)
g_poly : (ZMod p)[X] := X ^ p ^ n - X
hp : 1 < p
⊢ Module.finrank (ZMod p) (GaloisField p n) = n