awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
succ :
  HAdd.hAdd (α := ℕ)
      (∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * HPow.hPow (α := ℕ) 1 (p - (k + 1)) * (↑(p.choose (k + 1)) : ℕ)) 1 ≡
    1 [MOD p ^ m * p]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
rw [pow_succ, pow_mul, hd, add_pow, Finset.sum_range_succ', pow_zero, one_mul, one_pow,
      one_mul, Nat.choose_zero_right, Nat.cast_one]

Premises used: one_pow, pow_succ, pow_mul, pow_zero, add_pow, Nat.cast_one, Finset.sum_range_succ', Nat.choose_zero_right, one_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ HAdd.hAdd (α := ℕ)
      (∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * HPow.hPow (α := ℕ) 1 (p - (k + 1)) * (↑(p.choose (k + 1)) : ℕ)) 1 ≡
    1 [MOD p ^ m * p]

Tactic:
Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)

Premises used: Iff.mpr, Nat.modEq_zero_iff_dvd, OfNat.ofNat, Nat.ModEq.add_right
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
succ : p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * HPow.hPow (α := ℕ) 1 (p - (k + 1)) * (↑(p.choose (k + 1)) : ℕ)
⊢ HAdd.hAdd (α := ℕ)
      (∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * HPow.hPow (α := ℕ) 1 (p - (k + 1)) * (↑(p.choose (k + 1)) : ℕ)) 1 ≡
    1 [MOD p ^ m * p]

Tactic:
refine Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)

Premises used: Iff.mpr, Nat.modEq_zero_iff_dvd, OfNat.ofNat, Nat.ModEq.add_right
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
succ : p ^ m * p ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * (↑(p.choose (i + 1)) : ℕ))
⊢ p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * HPow.hPow (α := ℕ) 1 (p - (k + 1)) * (↑(p.choose (k + 1)) : ℕ)

Tactic:
simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]

Premises used: one_pow, Finset.mul_sum, mul_assoc, mul_one, pow_succ'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * (↑(p.choose (i + 1)) : ℕ))

Tactic:
mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)

Premises used: dvd_mul_of_dvd_right, mul_dvd_mul_left, HPow.hPow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
succ : ∀ (k : ℕ) (hk : k ∈ range p), p ∣ (p ^ m * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
⊢ p ^ m * p ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * (↑(p.choose (i + 1)) : ℕ))

Tactic:
refine mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)

Premises used: dvd_mul_of_dvd_right, mul_dvd_mul_left, HPow.hPow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
k : ℕ
hk : k ∈ range p
succ :
  ∀ (hd : (1 + p * a) ^ HPow.hPow (β := ℕ) p 0 = HPow.hPow (β := ℕ) p 0 * d + 1),
    p ∣ (HPow.hPow (β := ℕ) p 0 * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
succ₁ :
  ∀ (n : ℕ) (hd : (1 + p * a) ^ p ^ (n + 1) = p ^ (n + 1) * d + 1),
    p ∣ (p ^ (n + 1) * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
⊢ p ∣ (p ^ m * d) ^ k * (↑(p.choose (k + 1)) : ℕ)

Tactic:
cases m
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a d k : ℕ
hk : k ∈ range p
hd : (1 + p * a) ^ HPow.hPow (β := ℕ) p 0 = HPow.hPow (β := ℕ) p 0 * d + 1
⊢ p * a = d

Tactic:
rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd

Premises used: add_left_inj, add_comm, pow_zero, pow_one, one_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a d k : ℕ
hk : k ∈ range p
hd : p * a = d
succ :
  ∀ (hk : 0 ∈ range p),
    p ∣ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) p 0 * d) 0 * (↑(p.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℕ)
succ₁ : ∀ (n : ℕ) (hk : n + 1 ∈ range p), p ∣ (HPow.hPow (β := ℕ) p 0 * d) ^ (n + 1) * (↑(p.choose (n + 1 + 1)) : ℕ)
⊢ p ∣ (HPow.hPow (β := ℕ) p 0 * d) ^ k * (↑(p.choose (k + 1)) : ℕ)

Tactic:
cases k
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a d : ℕ
hd : p * a = d
hk : 0 ∈ range p
⊢ p ∣ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) p 0 * d) 0 * (↑(p.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℕ)

Tactic:
simp [← hd, mul_assoc, pow_succ']

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a d : ℕ
hd : p * a = d
n : ℕ
hk : n + 1 ∈ range p
⊢ p ∣ (HPow.hPow (β := ℕ) p 0 * d) ^ (n + 1) * (↑(p.choose (n + 1 + 1)) : ℕ)

Tactic:
simp [← hd, mul_assoc, pow_succ']

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a d k : ℕ
hk : k ∈ range p
n : ℕ
hd : (1 + p * a) ^ p ^ (n + 1) = p ^ (n + 1) * d + 1
succ : ∀ (hk : 0 ∈ range p), p ∣ HPow.hPow (β := ℕ) (p ^ (n + 1) * d) 0 * (↑(p.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℕ)
succ₁ : ∀ (n_1 : ℕ) (hk : n_1 + 1 ∈ range p), p ∣ (p ^ (n + 1) * d) ^ (n_1 + 1) * (↑(p.choose (n_1 + 1 + 1)) : ℕ)
⊢ p ∣ (p ^ (n + 1) * d) ^ k * (↑(p.choose (k + 1)) : ℕ)

Tactic:
cases k
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a d n : ℕ
hd : (1 + p * a) ^ p ^ (n + 1) = p ^ (n + 1) * d + 1
hk : 0 ∈ range p
⊢ p ∣ HPow.hPow (β := ℕ) (p ^ (n + 1) * d) 0 * (↑(p.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℕ)

Tactic:
simp [mul_assoc, pow_succ']

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a d n : ℕ
hd : (1 + p * a) ^ p ^ (n + 1) = p ^ (n + 1) * d + 1
n_1 : ℕ
hk : n_1 + 1 ∈ range p
⊢ p ∣ (p ^ (n + 1) * d) ^ (n_1 + 1) * (↑(p.choose (n_1 + 1 + 1)) : ℕ)

Tactic:
simp [mul_assoc, pow_succ']

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p m a : ℕ
zero : (1 + p * a) ^ HPow.hPow (β := ℕ) p 0 ≡ 1 [MOD HPow.hPow (β := ℕ) p 0]
succ : ∀ (m : ℕ) (hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]), (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
⊢ (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]

Tactic:
induction m with
  | zero => exact Nat.modEq_one
  | succ m hm =>
    rw [Nat.ModEq.comm, add_comm, Nat.modEq_iff_dvd' (Nat.one_le_pow' _ _)] at hm
    obtain ⟨d, hd⟩ := hm
    rw [tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _), add_comm] at hd
    rw [pow_succ, pow_mul, hd, add_pow, Finset.sum_range_succ', pow_zero, one_mul, one_pow,
      one_mul, Nat.choose_zero_right, Nat.cast_one]
    refine Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)
    simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]
    refine mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)
    cases m
    · rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd
      cases k <;> simp [← hd, mul_assoc, pow_succ']
    · cases k <;> simp [mul_assoc, pow_succ']

Premises used: Iff.mpr, one_pow, Nat.modEq_one, Finset.mul_sum, pow_succ, mul_assoc, add_left_inj, Nat.modEq_iff_dvd', add_comm, pow_mul, tsub_eq_iff_eq_add_of_le, pow_zero, Nat.one_le_pow', Nat.ModEq.comm, pow_one, add_pow, mul_one, Nat.modEq_zero_iff_dvd, OfNat.ofNat, Nat.ModEq.add_right, Nat.cast_one, Finset.sum_range_succ', Nat.choose_zero_right, pow_succ', one_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
inl : ∀ (hn : 0 = p ^ k) (a : ZMod 0) (ha : (orderOf a).Coprime 0), a = 1 ∨ IsUnit (a - 1)
inr : ∀ (hn0 : n ≠ 0), a = 1 ∨ IsUnit (a - 1)
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
rcases eq_or_ne n 0 with rfl | hn0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p k : ℕ
inst : Fact (Nat.Prime p)
hn : 0 = p ^ k
a : ZMod 0
ha : (orderOf a).Coprime 0
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
Or.inl (orderOf_eq_one_iff.mp ((orderOf a).coprime_zero_right.mp ha))

Premises used: Nat.coprime_zero_right, orderOf, Iff.mp, Or.inl, orderOf_eq_one_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p k : ℕ
inst : Fact (Nat.Prime p)
hn : 0 = p ^ k
a : ZMod 0
ha : (orderOf a).Coprime 0
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
exact Or.inl (orderOf_eq_one_iff.mp ((orderOf a).coprime_zero_right.mp ha))

Premises used: Nat.coprime_zero_right, orderOf, Iff.mp, Or.inl, orderOf_eq_one_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
inr : ∀ (ha : (orderOf (G := ZMod n) 0).Coprime n), Eq (α := ZMod n) 0 1 ∨ IsUnit (HSub.hSub (α := ZMod n) 0 1)
inr₁ : ∀ (ha0 : a ≠ 0), a = 1 ∨ IsUnit (a - 1)
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
rcases eq_or_ne a 0 with rfl | ha0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
ha : (orderOf (G := ZMod n) 0).Coprime n
⊢ Eq (α := ZMod n) 0 1 ∨ IsUnit (HSub.hSub (α := ZMod n) 0 1)

Tactic:
Or.inr (zero_sub (1 : ZMod n) ▸ isUnit_neg_one)

Premises used: Eq.rec, isUnit_neg_one, OfNat.ofNat, Eq.symm, Or.inr, zero_sub
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
ha : (orderOf (G := ZMod n) 0).Coprime n
⊢ Eq (α := ZMod n) 0 1 ∨ IsUnit (HSub.hSub (α := ZMod n) 0 1)

Tactic:
exact Or.inr (zero_sub (1 : ZMod n) ▸ isUnit_neg_one)

Premises used: Or.inr
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn0⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
ha0 : a ≠ 0
this : NeZero n
inr :
  ∀ (a : ℕ) (ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n) (ha0 : Ne (α := ZMod n) (↑a : ZMod n) 0),
    Eq (α := ZMod n) (↑a : ZMod n) 1 ∨ IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
⊢ a = 1 ∨ IsUnit (a - 1)

Tactic:
obtain ⟨a, rfl⟩ := ZMod.natCast_zmod_surjective a

Premises used: ZMod.natCast_zmod_surjective, rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
ha0 : Ne (α := ZMod n) (↑a : ZMod n) 0
inr : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1) → orderOf (G := ZMod n) (↑a : ZMod n) = 1
⊢ Eq (α := ZMod n) (↑a : ZMod n) 1 ∨ IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)

Tactic:
rw [← orderOf_eq_one_iff, or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right, orderOf_eq_one_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
ha0 : Ne (α := ZMod n) (↑a : ZMod n) 0
⊢ ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1) → orderOf (G := ZMod n) (↑a : ZMod n) = 1

Tactic:
fun h ↦ ha.eq_one_of_dvd ?_

Premises used: Nat.Coprime.eq_one_of_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
ha0 : Ne (α := ZMod n) (↑a : ZMod n) 0
inr : ∀ (h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)), orderOf (G := ZMod n) (↑a : ZMod n) ∣ n
⊢ ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1) → orderOf (G := ZMod n) (↑a : ZMod n) = 1

Tactic:
refine fun h ↦ ha.eq_one_of_dvd ?_

Premises used: Nat.Coprime.eq_one_of_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
ha0 : Ne (α := ZMod n) (↑a : ZMod n) 0
h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
inr : a ^ p ^ k ≡ 1 [MOD p ^ k]
⊢ orderOf (G := ZMod n) (↑a : ZMod n) ∣ n

Tactic:
rw [orderOf_dvd_iff_pow_eq_one, ← Nat.cast_pow, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff, hn]

Premises used: ZMod.natCast_eq_natCast_iff, Nat.cast_pow, orderOf_dvd_iff_pow_eq_one, Nat.cast_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
ha0 : Ne (α := ZMod n) (↑a : ZMod n) 0
h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
contrapose! : ∀ (ha0 : a < 1), Eq (α := ZMod n) (↑a : ZMod n) 0
⊢ 1 ≤ a

Tactic:
contrapose! ha0
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
ha0 : a < 1
rw : Eq (α := ZMod n) (↑0 : ZMod n) 0
rw₁ rw₂ : Eq (α := ZMod n) 0 0
⊢ Eq (α := ZMod n) (↑a : ZMod n) 0

Tactic:
rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]

Premises used: Nat.lt_one_iff, Iff.mp, Nat.cast_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
ha0 : Ne (α := ZMod n) (↑a : ZMod n) 0
h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
⊢ 1 ≤ a

Tactic:
replace ha0 : 1 ≤ a := by
    contrapose! ha0
    rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
ha0 : 1 ≤ a
⊢ ¬(a - 1).Coprime (p ^ k)

Tactic:
rw [← Nat.cast_one, ← Nat.cast_sub ha0, ZMod.isUnit_iff_coprime, hn] at h

Premises used: ZMod.isUnit_iff_coprime, Nat.cast_sub, Nat.cast_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
ha0 : 1 ≤ a
h₁ : ¬(a - 1).Coprime (p ^ k)
⊢ 1 ≤ a

Tactic:
rw [← Nat.cast_one, ← Nat.cast_sub ha0, ZMod.isUnit_iff_coprime, hn] at h

Premises used: ZMod.isUnit_iff_coprime, Nat.cast_sub, Nat.cast_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
inr : ∀ (b : ℕ) (hb : a - 1 = p * b), a ^ p ^ k ≡ 1 [MOD p ^ k]
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
obtain ⟨b, hb⟩ := not_imp_comm.mp (Nat.Prime.coprime_pow_of_not_dvd Fact.out) h

Premises used: not_imp_comm, Iff.mp, Fact.out, Nat.Prime.coprime_pow_of_not_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a - 1 = p * b
⊢ a = 1 + p * b

Tactic:
rw [tsub_eq_iff_eq_add_of_le ha0, add_comm] at hb

Premises used: add_comm, tsub_eq_iff_eq_add_of_le
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a = 1 + p * b
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
hb ▸ pow_pow_modEq_one p k b

Premises used: pow_pow_modEq_one, Eq.rec, Eq.symm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
hn0 : n ≠ 0
this : NeZero n
a : ℕ
ha : (orderOf (G := ZMod n) (↑a : ZMod n)).Coprime n
h : ¬(a - 1).Coprime (p ^ k)
ha0 : 1 ≤ a
b : ℕ
hb : a = 1 + p * b
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]

Tactic:
exact hb ▸ pow_pow_modEq_one p k b
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
K : Type u_4
inst_1 : DivisionRing K
inst_2 : CharP K p
x : K
⊢ Membership.mem (γ := Subfield K) ⊥ x ↔ ∃ (n : ℤ), (↑n : K) = x

Tactic:
simp [← fieldRange_castHom_eq_bot p, ZMod.intCast_surjective.exists]

Premises used: Function.Surjective.exists, ZMod.fieldRange_castHom_eq_bot, ZMod.intCast_surjective
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
rw : Nat.card.{u_3} ↥(RingHom.fieldRange (K := ZMod p) (castHom ⋯ F)) = p
rw₁ : Nat.card (ZMod p) = p
rw₂ rw₃ : p = p
⊢ Nat.card.{u_3} ↥⊥ = p

Tactic:
rw [← fieldRange_castHom_eq_bot p,
    ← Nat.card_eq_of_bijective _ (RingHom.rangeRestrictField_bijective _), Nat.card_zmod]

Premises used: RingHom.rangeRestrictField_bijective, Nat.card_zmod, Nat.card_eq_of_bijective, ZMod.fieldRange_castHom_eq_bot
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : F
simp_rw :
  (∃ (a : ZMod p),
      ({ toFun := (⇑(castHom ⋯ F) : (a : ZMod p) → F), inj' := ⋯ : ZMod p ↪ F } : (a : ZMod p) → F) a = x) ↔
    Membership.mem (γ := Subfield F) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ F)) x
⊢ x ∈ Finset.map { toFun := (⇑(castHom ⋯ F) : (a : ZMod p) → F), inj' := ⋯ : ZMod p ↪ F } univ ↔
    Membership.mem (γ := Subfield F) ⊥ x

Tactic:
simp_rw [Finset.mem_map, mem_univ, true_and, ← fieldRange_castHom_eq_bot p]

Premises used: Finset.mem_univ, Finset.mem_map, ZMod.fieldRange_castHom_eq_bot, true_and
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : F
⊢ (∃ (a : ZMod p),
      ({ toFun := (⇑(castHom ⋯ F) : (a : ZMod p) → F), inj' := ⋯ : ZMod p ↪ F } : (a : ZMod p) → F) a = x) ↔
    Membership.mem (γ := Subfield F) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ F)) x

Tactic:
rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : Fintype ↥⊥ := fintypeBot F p
rw : (HPow.hPow (α := (↥⊥)[X]) X (Fintype.card.{u_3} ↥⊥) - X).roots
rw₁ : Fintype ↥⊥
| (HPow.hPow (α := (↥⊥)[X]) X p - X).roots

Tactic:
rw [← card_bot F p, ← Fintype.card_eq_nat_card]

Premises used: Subfield.card_bot, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : Fintype ↥⊥ := fintypeBot F p
conv_lhs : (HPow.hPow (α := (↥⊥)[X]) X (Fintype.card.{u_3} ↥⊥) - X).roots = Finset.val univ
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).roots = Finset.val univ

Tactic:
conv_lhs => rw [← card_bot F p, ← Fintype.card_eq_nat_card]

Premises used: Subfield.card_bot, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : Fintype ↥⊥ := fintypeBot F p
⊢ (HPow.hPow (α := (↥⊥)[X]) X (Fintype.card.{u_3} ↥⊥) - X).roots = Finset.val univ

Tactic:
FiniteField.roots_X_pow_card_sub_X _

Premises used: Set.Mem, FiniteField.roots_X_pow_card_sub_X, Subring.mk'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : Fintype ↥⊥ := fintypeBot F p
⊢ (HPow.hPow (α := (↥⊥)[X]) X (Fintype.card.{u_3} ↥⊥) - X).roots = Finset.val univ

Tactic:
exact FiniteField.roots_X_pow_card_sub_X _

Premises used: FiniteField.roots_X_pow_card_sub_X
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : Fintype ↥⊥ := fintypeBot F p
rw : (HPow.hPow (α := (↥⊥)[X]) X p - X).roots.card = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
rw₁ : Multiset.card.{u_3} (α := ↥⊥) (Finset.val univ) = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
rw₂ : Finset.card.{u_3} (α := ↥⊥) univ = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
rw₃ : Fintype.card.{u_3} ↥⊥ = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
rw₄ : Fintype.card.{u_3} ↥⊥ = p
rw₅ : Nat.card.{u_3} ↥⊥ = p
rw₆ rw₇ : p = p
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).Splits

Tactic:
rw [splits_iff_card_roots, roots_X_pow_char_sub_X_bot, ← Finset.card_def, Finset.card_univ,
    FiniteField.X_pow_card_sub_X_natDegree_eq _ (Fact.out (p := p.Prime)).one_lt,
    Fintype.card_eq_nat_card, card_bot F p]

Premises used: Finset.card_univ, Nat.Prime.one_lt, Subfield.roots_X_pow_char_sub_X_bot, Polynomial.splits_iff_card_roots, FiniteField.X_pow_card_sub_X_natDegree_eq, Finset.card_def, Subfield.card_bot, Fact.out, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : F
⊢ x ∈ (Polynomial.map (subtype ⊥) (HPow.hPow (α := (↥⊥)[X]) X p - X)).roots ↔
    ∃ (a : ↥⊥), Membership.mem (γ := Multiset ↥⊥) (Finset.val univ) a ∧ (subtype ⊥ : (a : ↥⊥) → F) a = x

Tactic:
have := roots_X_pow_char_sub_X_bot F p ▸
      (splits_bot F p).roots_map (Subfield.subtype _) ▸ Multiset.mem_map (b := x)
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : F
this :
  x ∈ (Polynomial.map (subtype ⊥) (HPow.hPow (α := (↥⊥)[X]) X p - X)).roots ↔
    ∃ (a : ↥⊥), Membership.mem (γ := Multiset ↥⊥) (Finset.val univ) a ∧ (subtype ⊥ : (a : ↥⊥) → F) a = x
⊢ Membership.mem (γ := Subfield F) ⊥ x ↔ x ^ p = x

Tactic:
simpa [sub_eq_zero, iff_comm, FiniteField.X_pow_card_sub_X_ne_zero F (Fact.out : p.Prime).one_lt]

Premises used: Nat.Prime.one_lt, sub_eq_zero, iff_comm, FiniteField.X_pow_card_sub_X_ne_zero, Fact.out
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Finite F
hF : ringChar F = 2
a : F
⊢ IsSquare a

Tactic:
have : CharP F 2 := ringChar.of_eq hF
  isSquare_of_charTwo' a

Premises used: ringChar.of_eq, isSquare_of_charTwo'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Finite F
hF : ringChar F ≠ 2
h : Function.Injective (β := F) fun (x : F) ↦ x * x
⊢ HMul.hMul (α := F) (-1) (-1) = HMul.hMul (α := F) 1 1

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Finite F
hF : ringChar F ≠ 2
⊢ ¬Function.Injective (β := F) fun (x : F) ↦ x * x

Tactic:
have h : ¬Function.Injective fun x : F ↦ x * x := fun h ↦
    h.ne (Ring.neg_one_ne_one_of_char_ne_two hF) <| by simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Finite F
hF : ringChar F ≠ 2
h : ¬Function.Injective (β := F) fun (x : F) ↦ x * x
⊢ ∃ (a : F), ¬IsSquare a

Tactic:
simpa [Finite.injective_iff_surjective, Function.Surjective, IsSquare, eq_comm] using h

Premises used: eq_comm, IsSquare, Finite.injective_iff_surjective, Function.Surjective
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
rcases :
  ∀ (n : ℕ+) (hp : Nat.Prime (ringChar F)) (h : Fintype.card F = ringChar F ^ (↑n : ℕ)),
    ringChar F = 2 ↔ Fintype.card F % 2 = 0
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0

Tactic:
rcases FiniteField.card F (ringChar F) with ⟨n, hp, h⟩

Premises used: FiniteField.card, ringChar
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ (↑n : ℕ)
rw : ringChar F = 2 ↔ ringChar F = 2 ∧ (↑n : ℕ) ≠ 0
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0

Tactic:
rw [h, ← Nat.even_iff, Nat.even_pow, hp.even_iff]

Premises used: Nat.Prime.even_iff, Nat.even_pow, Nat.even_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
n : ℕ+
hp : Nat.Prime (ringChar F)
h : Fintype.card F = ringChar F ^ (↑n : ℕ)
⊢ ringChar F = 2 ↔ ringChar F = 2 ∧ (↑n : ℕ) ≠ 0

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F = 2
⊢ Fintype.card F % 2 = 0

Tactic:
even_card_iff_char_two.mp hF

Premises used: Iff.mp, FiniteField.even_card_iff_char_two
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
⊢ Fintype.card F % 2 = 1

Tactic:
Nat.mod_two_ne_zero.mp (mt even_card_iff_char_two.mpr hF)

Premises used: Iff.mpr, mt, Iff.mp, FiniteField.even_card_iff_char_two, Nat.mod_two_ne_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ a ^ (Fintype.card F - 1) = 1

Tactic:
have h₁ := FiniteField.pow_card_sub_one_eq_one a ha