awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2
g : (ZMod p)[X] :=
  HSub.hSub (β := (ZMod p)[X]) (HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2)
    ((C : (a : ZMod p) → (ZMod p)[X]) x : (ZMod p)[X])
a b : ZMod p
hab : eval a f + eval b g = 0
inr : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - x = 0
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = x

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2
g : (ZMod p)[X] :=
  HSub.hSub (β := (ZMod p)[X]) (HPow.hPow (α := (ZMod p)[X]) (β := ℕ) X 2)
    ((C : (a : ZMod p) → (ZMod p)[X]) x : (ZMod p)[X])
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 - x = 0

Tactic:
simpa only [f, g, eval_C, eval_X, eval_pow, eval_sub, ← add_sub_assoc] using hab

Premises used: add_sub_assoc, Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_pow, Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
rcases :
  ∀ (a b : ZMod p) (hx : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)),
    ∃ (a : ℕ) (b : ℕ),
      a ≤ p / 2 ∧
        b ≤ p / 2 ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ x [ZMOD (↑p : ℤ)]
⊢ ∃ (a : ℕ) (b : ℕ),
    a ≤ p / 2 ∧
      b ≤ p / 2 ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ x [ZMOD (↑p : ℤ)]

Tactic:
rcases ZMod.sq_add_sq p x with ⟨a, b, hx⟩

Premises used: Int.cast, ZMod.sq_add_sq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
⊢ ∃ (a : ℕ) (b : ℕ),
    a ≤ p / 2 ∧
      b ≤ p / 2 ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ x [ZMOD (↑p : ℤ)]

Tactic:
⟨a.valMinAbs.natAbs, b.valMinAbs.natAbs, ZMod.natAbs_valMinAbs_le _,
    ZMod.natAbs_valMinAbs_le _, ?_⟩

Premises used: ZMod.valMinAbs, ZMod.natAbs_valMinAbs_le, And.intro, Int.natAbs, Exists.intro
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
refine :
  HPow.hPow (α := ℤ) (β := ℕ) (↑a.valMinAbs.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b.valMinAbs.natAbs : ℤ) 2 ≡
    x [ZMOD (↑p : ℤ)]
⊢ ∃ (a : ℕ) (b : ℕ),
    a ≤ p / 2 ∧
      b ≤ p / 2 ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ x [ZMOD (↑p : ℤ)]

Tactic:
refine ⟨a.valMinAbs.natAbs, b.valMinAbs.natAbs, ZMod.natAbs_valMinAbs_le _,
    ZMod.natAbs_valMinAbs_le _, ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
⊢ HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
      HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
    (↑x : ZMod p)

Tactic:
rw [← a.coe_valMinAbs, ← b.coe_valMinAbs] at hx

Premises used: ZMod.coe_valMinAbs
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
      HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
    (↑x : ZMod p)
push_cast : HPow.hPow (β := ℕ) |a.valMinAbs| 2 + HPow.hPow (β := ℕ) |b.valMinAbs| 2 ≡ x [ZMOD (↑p : ℤ)]
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑a.valMinAbs.natAbs : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b.valMinAbs.natAbs : ℤ) 2 ≡
    x [ZMOD (↑p : ℤ)]

Tactic:
push_cast
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
      HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
    (↑x : ZMod p)
rw : Eq (α := ZMod p) (↑(HPow.hPow (β := ℕ) a.valMinAbs 2 + HPow.hPow (β := ℕ) b.valMinAbs 2) : ZMod p) (↑x : ZMod p)
⊢ HPow.hPow (β := ℕ) |a.valMinAbs| 2 + HPow.hPow (β := ℕ) |b.valMinAbs| 2 ≡ x [ZMOD (↑p : ℤ)]

Tactic:
rw [sq_abs, sq_abs, ← ZMod.intCast_eq_intCast_iff]

Premises used: ZMod.intCast_eq_intCast_iff, sq_abs
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
      HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
    (↑x : ZMod p)
⊢ Eq (α := ZMod p) (↑(HPow.hPow (β := ℕ) a.valMinAbs 2 + HPow.hPow (β := ℕ) b.valMinAbs 2) : ZMod p) (↑x : ZMod p)

Tactic:
mod_cast hx

Premises used: Int.cast, congrArg, ZMod.valMinAbs, Int.cast_pow, cast, Int.cast_add, ZMod.coe_valMinAbs, HPow.hPow, HAdd.hAdd, congr, Int.cast_pow._simp_1, Int.cast_add._simp_1, congrFun', OfNat.ofNat, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℤ
a b : ZMod p
hx :
  HPow.hPow (α := ZMod p) (β := ℕ) (↑a.valMinAbs : ZMod p) 2 +
      HPow.hPow (α := ZMod p) (β := ℕ) (↑b.valMinAbs : ZMod p) 2 =
    (↑x : ZMod p)
⊢ Eq (α := ZMod p) (↑(HPow.hPow (β := ℕ) a.valMinAbs 2 + HPow.hPow (β := ℕ) b.valMinAbs 2) : ZMod p) (↑x : ZMod p)

Tactic:
exact mod_cast hx
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Prime p)
x : ℕ
⊢ ∃ (a : ℕ) (b : ℕ), a ≤ p / 2 ∧ b ≤ p / 2 ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≡ x [MOD p]

Tactic:
simpa only [← Int.natCast_modEq_iff] using Nat.sq_add_sq_zmodEq p x

Premises used: Int.natCast_modEq_iff, Nat.cast, Nat.sq_add_sq_zmodEq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : IsDomain R
p : ℕ
inst_2 : NeZero p
inst_3 : CharP R p
x : ℤ
⊢ Fact (Nat.Prime p)

Tactic:
haveI := char_is_prime_of_pos R p
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : IsDomain R
p : ℕ
inst_2 : NeZero p
inst_3 : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
obtain :
  ∀ (a b : ZMod p) (hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)),
    ∃ (a : ℕ) (b : ℕ), HPow.hPow (α := R) (β := ℕ) (↑a : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b : R) 2 = (↑x : R)
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (α := R) (β := ℕ) (↑a : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b : R) 2 = (↑x : R)

Tactic:
obtain ⟨a, b, hab⟩ := ZMod.sq_add_sq p x

Premises used: Int.cast, ZMod.sq_add_sq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : IsDomain R
p : ℕ
inst_2 : NeZero p
inst_3 : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (α := R) (β := ℕ) (↑a : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b : R) 2 = (↑x : R)

Tactic:
⟨a.val, b.val, ?_⟩

Premises used: Exists.intro, ZMod.val
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : IsDomain R
p : ℕ
inst_2 : NeZero p
inst_3 : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
refine : HPow.hPow (α := R) (β := ℕ) (↑a.val : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b.val : R) 2 = (↑x : R)
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (α := R) (β := ℕ) (↑a : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b : R) 2 = (↑x : R)

Tactic:
refine ⟨a.val, b.val, ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : IsDomain R
p : ℕ
inst_2 : NeZero p
inst_3 : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = (↑x : ZMod p)
⊢ HPow.hPow (α := R) (β := ℕ) (↑a.val : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b.val : R) 2 = (↑x : R)

Tactic:
simpa using congr_arg (ZMod.castHom dvd_rfl R) hab

Premises used: congr_arg, dvd_rfl, DFunLike.coe, ZMod.castHom
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n : ℕ
x : (ZMod n)ˣ
zero : ∀ (x : (ZMod 0)ˣ), x ^ φ 0 = 1
succ : ∀ (n : ℕ) (x : (ZMod (n + 1))ˣ), x ^ φ (n + 1) = 1
⊢ x ^ φ n = 1

Tactic:
cases n
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
x : (ZMod 0)ˣ
zero : HPow.hPow (β := ℕ) x 0 = 1
zero₁ zero₂ : Eq (α := (ZMod 0)ˣ) 1 1
⊢ x ^ φ 0 = 1

Tactic:
rw [Nat.totient_zero, pow_zero]

Premises used: Nat.totient_zero, pow_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
n : ℕ
x : (ZMod (n + 1))ˣ
succ : x ^ Fintype.card (ZMod (n + 1))ˣ = 1
succ₁ succ₂ : Eq (α := (ZMod (n + 1))ˣ) 1 1
⊢ x ^ φ (n + 1) = 1

Tactic:
rw [← card_units_eq_totient, pow_card_eq_one]

Premises used: pow_card_eq_one, ZMod.card_units_eq_totient
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
x n : ℕ
h : x.Coprime n
rw : Eq (α := ZMod n) (↑(x ^ φ n) : ZMod n) (↑1 : ZMod n)
⊢ x ^ φ n ≡ 1 [MOD n]

Tactic:
rw [← ZMod.natCast_eq_natCast_iff]

Premises used: ZMod.natCast_eq_natCast_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
⊢ x' ^ φ n = 1

Tactic:
have := ZMod.pow_totient x'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : x' ^ φ n = 1
⊢ (↑(x' ^ φ n) : ZMod n) = (↑1 : ZMod n)

Tactic:
apply_fun ((fun (x : Units (ZMod n)) => (x : ZMod n)) : Units (ZMod n) → ZMod n) at this

Premises used: Units.val
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : (↑(x' ^ φ n) : ZMod n) = (↑1 : ZMod n)
⊢ Eq (α := ZMod n) (↑(x ^ φ n) : ZMod n) (↑1 : ZMod n)

Tactic:
simpa only [Nat.succ_eq_add_one, Nat.cast_pow, Units.val_one, Nat.cast_one,
    coe_unitOfCoprime, Units.val_pow_eq_pow_val]

Premises used: Nat.succ_eq_add_one, Units.val_one, ZMod.coe_unitOfCoprime, Nat.cast_pow, Units.val_pow_eq_pow_val, Nat.cast_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
p : ℕ
inst : Fact (Nat.Prime p)
n : ZMod p
h : Membership.mem (γ := Subfield (ZMod p)) ⊤ n
this : Membership.mem (γ := Subfield (ZMod p)) ⊥ (HSMul.hSMul (α := ℤ) (β := ZMod p) (↑n.val : ℤ) 1)
rwa :
  ∀ (this : Membership.mem (γ := Subfield (ZMod p)) ⊥ (HSMul.hSMul (β := ZMod p) n.val 1)),
    Membership.mem (γ := Subfield (ZMod p)) ⊥ n
rwa₁ :
  ∀ (this : Membership.mem (γ := Subfield (ZMod p)) ⊥ (↑n.val : ZMod p)), Membership.mem (γ := Subfield (ZMod p)) ⊥ n
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : Membership.mem (γ := Subfield (ZMod p)) ⊥ n), Membership.mem (γ := Subfield (ZMod p)) ⊥ n
⊢ Membership.mem (γ := Subfield (ZMod p)) ⊥ n

Tactic:
rwa [natCast_zsmul, Nat.smul_one_eq_cast, ZMod.natCast_zmod_val] at this

Premises used: ZMod.natCast_zmod_val, Nat.smul_one_eq_cast, natCast_zsmul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
inst_1 : DivisionRing K
inst_2 : CharP K p
rw : Eq.{u_1 + 1} (α := Subfield K) (Subfield.map (K := ZMod p) (castHom ⋯ K) ⊤) ⊥
rw₁ :
  Eq.{u_1 + 1} (α := Subfield K) (Subfield.map (K := ZMod p) (castHom ⋯ K) ⊤)
    (Subfield.map (K := ZMod p) (castHom ⋯ K) ⊥)
rw₂ : ZMod p →+* K
rw₃ :
  Eq.{u_1 + 1} (α := Subfield K) (Subfield.map (K := ZMod p) (castHom ⋯ K) ⊤)
    (Subfield.map (K := ZMod p) (castHom ⋯ K) ⊤)
rw₄ : Subfield (ZMod p)
rw₅ : ZMod p →+* K
rw₆ :
  Eq.{u_1 + 1} (α := Subfield K) (Subfield.map (K := ZMod p) (castHom ⋯ K) ⊤)
    (Subfield.map (K := ZMod p) (castHom ⋯ K) ⊤)
rw₇ : Subfield (ZMod p)
rw₈ : ZMod p →+* K
⊢ Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ K)) ⊥

Tactic:
rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]

Premises used: Subfield.map_bot, Bot.bot, RingHom.fieldRange_eq_map, Subsingleton.elim
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ Fintype.card (ZMod p) = x

Tactic:
have h := FiniteField.pow_card x
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : x ^ p = x), x ^ p = x
⊢ x ^ p = x

Tactic:
rwa [ZMod.card p] at h

Premises used: ZMod.card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ HPow.hPow (β := ℕ) p 0 = x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ZMod p
n : ℕ
ih : x ^ p ^ n = x
⊢ x ^ p ^ (n + 1) = x

Tactic:
simp [pow_succ, pow_mul, ih, pow_card]

Premises used: pow_succ, ZMod.pow_card, pow_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
n : ℕ
x : ZMod p
zero : x ^ HPow.hPow (β := ℕ) p 0 = x
succ : ∀ (n : ℕ) (ih : x ^ p ^ n = x), x ^ p ^ (n + 1) = x
⊢ x ^ p ^ n = x

Tactic:
induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]

Premises used: pow_succ, ZMod.pow_card, pow_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a :
  ∀ (a : ZMod p),
    Eq (α := ZMod p) ((frobenius (ZMod p) p : (a : ZMod p) → ZMod p) a : ZMod p)
      ((RingHom.id (ZMod p) : (a : ZMod p) → ZMod p) a : ZMod p)
⊢ Eq (α := ZMod p →+* ZMod p) (frobenius (ZMod p) p) (RingHom.id (ZMod p))

Tactic:
ext a
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
a₁ : a ^ p = (RingHom.id (ZMod p) : (a : ZMod p) → ZMod p) a
a₂ : a = (RingHom.id (ZMod p) : (a : ZMod p) → ZMod p) a
a₃ a₄ : a = a
⊢ Eq (α := ZMod p) ((frobenius (ZMod p) p : (a : ZMod p) → ZMod p) a : ZMod p)
    ((RingHom.id (ZMod p) : (a : ZMod p) → ZMod p) a : ZMod p)

Tactic:
rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]

Premises used: RingHom.id_apply, ZMod.pow_card, frobenius_def
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Fintype.card (ZMod p) - 1 = p - 1
rw₁ rw₂ : p - 1 = p - 1
⊢ Fintype.card (ZMod p)ˣ = p - 1

Tactic:
rw [Fintype.card_units, card]

Premises used: Fintype.card_units, ZMod.card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : (ZMod p)ˣ
rw : a ^ Fintype.card (ZMod p)ˣ = 1
rw₁ rw₂ : Eq (α := (ZMod p)ˣ) 1 1
⊢ a ^ (p - 1) = 1

Tactic:
rw [← card_units p, pow_card_eq_one]

Premises used: pow_card_eq_one, ZMod.card_units
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (Fintype.card (ZMod p) - 1) = 1

Tactic:
have h := FiniteField.pow_card_sub_one_eq_one a ha
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
h : a ^ (Fintype.card (ZMod p) - 1) = 1
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : a ^ (p - 1) = 1), a ^ (p - 1) = 1
⊢ a ^ (p - 1) = 1

Tactic:
rwa [ZMod.card p] at h

Premises used: ZMod.card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
pos : ∀ (ha : a ≠ 0), a ^ (p - 1) = 1
neg : ∀ (ha : ¬a ≠ 0), a ^ (p - 1) = 0
⊢ a ^ (p - 1) = if a ≠ 0 then 1 else 0

Tactic:
split_ifs with ha
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1

Tactic:
pow_card_sub_one_eq_one ha

Premises used: ZMod.pow_card_sub_one_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1

Tactic:
exact pow_card_sub_one_eq_one ha

Premises used: ZMod.pow_card_sub_one_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : ¬a ≠ 0
⊢ a ^ (p - 1) = 0

Tactic:
simp [of_not_not ha, (Fact.out : p.Prime).one_lt, tsub_eq_zero_iff_le]

Premises used: Nat.Prime.one_lt, tsub_eq_zero_iff_le, of_not_not, Fact.out
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
u : (ZMod p)ˣ
⊢ orderOf u ∣ p - 1

Tactic:
orderOf_dvd_of_pow_eq_one <| units_pow_card_sub_one_eq_one _ _

Premises used: ZMod.units_pow_card_sub_one_eq_one, orderOf_dvd_of_pow_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ orderOf a ∣ p - 1

Tactic:
orderOf_dvd_of_pow_eq_one <| pow_card_sub_one_eq_one ha

Premises used: orderOf_dvd_of_pow_eq_one, ZMod.pow_card_sub_one_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : (ZMod p)[X]
⊢ (expand (ZMod p) (Fintype.card (ZMod p)) : (a : (ZMod p)[X]) → (ZMod p)[X]) f = f ^ Fintype.card (ZMod p)

Tactic:
have h := FiniteField.expand_card f
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : (expand (ZMod p) (Fintype.card (ZMod p)) : (a : (ZMod p)[X]) → (ZMod p)[X]) f = f ^ Fintype.card (ZMod p)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (h : (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) f = f ^ p),
    (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) f = f ^ p
⊢ (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) f = f ^ p

Tactic:
rwa [ZMod.card p] at h

Premises used: ZMod.card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
⊢ Fact (Nat.Prime p)

Tactic:
haveI : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
this : Fact (Nat.Prime p)
rw : IsCoprime (↑p : ℤ) n
⊢ ¬Eq (α := ZMod p) (↑n : ZMod p) 0

Tactic:
rw [CharP.intCast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]

Premises used: Nat.prime_iff_prime_int, Prime.coprime_iff_not_dvd, Iff.mp, CharP.intCast_eq_zero_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p : ℤ) n

Tactic:
hpn.symm

Premises used: IsCoprime.symm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p : ℤ) n

Tactic:
exact hpn.symm

Premises used: IsCoprime.symm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
this : Fact (Nat.Prime p)
⊢ ¬Eq (α := ZMod p) (↑n : ZMod p) 0

Tactic:
have : ¬(n : ZMod p) = 0 := by
    rw [CharP.intCast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]
    · exact hpn.symm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
this_1 : Fact (Nat.Prime p)
this : ¬Eq (α := ZMod p) (↑n : ZMod p) 0
⊢ n ^ (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]

Tactic:
simpa [← ZMod.intCast_eq_intCast_iff] using ZMod.pow_card_sub_one_eq_one this

Premises used: ZMod.pow_card_sub_one_eq_one, ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
⊢ (↑p : ℤ) ∣ n ^ (p - 1) - 1

Tactic:
(ModEq.pow_card_sub_one_eq_one hp hpn).symm.dvd

Premises used: Int.ModEq.symm, Int.ModEq.dvd, Int.ModEq.pow_card_sub_one_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
⊢ Fact (Nat.Prime p)

Tactic:
haveI : Fact p.Prime := ⟨hp⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
this : Fact (Nat.Prime p)
⊢ n ^ p ≡ n [ZMOD (↑p : ℤ)]

Tactic:
simp [← ZMod.intCast_eq_intCast_iff]

Premises used: ZMod.intCast_eq_intCast_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
⊢ (↑p : ℤ) ∣ n ^ p - n

Tactic:
(ModEq.pow_prime_eq_self hp n).symm.dvd

Premises used: Int.ModEq.symm, Int.ModEq.dvd, Int.ModEq.pow_prime_eq_self
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p x y : ℕ
hp : Nat.Prime p
h : p - 1 ∣ x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
rw : ∀ (h : (p - 1) * ((x - y) / (p - 1)) = x - y) (hxy : y ≤ x) (hy : 0 < y) (n : ℤ), n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]

Tactic:
rw [← Nat.mul_div_eq_iff_dvd] at h

Premises used: Nat.mul_div_eq_iff_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
pos : ∀ (hn : n ≡ 0 [ZMOD (↑p : ℤ)]), n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
neg : ∀ (hn : ¬n ≡ 0 [ZMOD (↑p : ℤ)]), n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]

Tactic:
by_cases hn : n ≡ 0 [ZMOD p]
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : n ≡ 0 [ZMOD (↑p : ℤ)]
pos : HPow.hPow (α := ℤ) 0 x ≡ HPow.hPow (α := ℤ) 0 y [ZMOD (↑p : ℤ)]
pos₁ : 0 ≡ HPow.hPow (α := ℤ) 0 y [ZMOD (↑p : ℤ)]
pos₂ pos₃ : 0 ≡ 0 [ZMOD (↑p : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]

Tactic:
grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']

Premises used: LT.lt.ne', LT.lt.trans_le, zero_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : ¬n ≡ 0 [ZMOD (↑p : ℤ)]
⊢ IsCoprime (↑p : ℤ) n

Tactic:
rw [Int.modEq_zero_iff_dvd, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at hn

Premises used: Nat.prime_iff_prime_int, Prime.coprime_iff_not_dvd, Iff.mp, Int.modEq_zero_iff_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p : ℤ) n
neg : n ^ (x - y) * n ^ y ≡ n ^ y [ZMOD (↑p : ℤ)]
neg₁ : n ^ ((p - 1) * ((x - y) / (p - 1))) * n ^ y ≡ n ^ y [ZMOD (↑p : ℤ)]
neg₂ : (n ^ (p - 1)) ^ ((x - y) / (p - 1)) * n ^ y ≡ n ^ y [ZMOD (↑p : ℤ)]
neg₃ : HPow.hPow (α := ℤ) 1 ((x - y) / (p - 1)) * n ^ y ≡ n ^ y [ZMOD (↑p : ℤ)]
neg₄ : 1 * n ^ y ≡ n ^ y [ZMOD (↑p : ℤ)]
neg₅ neg₆ : n ^ y ≡ n ^ y [ZMOD (↑p : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]

Tactic:
grw [← pow_sub_mul_pow n hxy, ← h, pow_mul, Int.ModEq.pow_card_sub_one_eq_one hp hn.symm,
      one_pow, one_mul]

Premises used: one_pow, IsCoprime.symm, pow_sub_mul_pow, pow_mul, Int.ModEq.pow_card_sub_one_eq_one, one_mul
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Prime p
n : ℕ
hpn : n.Coprime p
rw : HPow.hPow (α := ℤ) (↑n : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]
⊢ n ^ (p - 1) ≡ 1 [MOD p]

Tactic:
rw [← Int.natCast_modEq_iff, Nat.cast_pow, Nat.cast_one]

Premises used: Int.natCast_modEq_iff, Nat.cast_pow, Nat.cast_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Prime p
n : ℕ
hpn : n.Coprime p
⊢ HPow.hPow (α := ℤ) (↑n : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]

Tactic:
Int.ModEq.pow_card_sub_one_eq_one hp (isCoprime_iff_coprime.mpr hpn)

Premises used: Iff.mpr, Nat.isCoprime_iff_coprime, Int.ModEq.pow_card_sub_one_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Prime p
n : ℕ
hpn : n.Coprime p
⊢ HPow.hPow (α := ℤ) (↑n : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]

Tactic:
exact Int.ModEq.pow_card_sub_one_eq_one hp (isCoprime_iff_coprime.mpr hpn)

Premises used: Iff.mpr, Nat.isCoprime_iff_coprime, Int.ModEq.pow_card_sub_one_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p : ℕ
hp : Prime p
n : ℕ
hpn : n.Coprime p
⊢ (n ^ (p - 1) - 1) % p = 0

Tactic:
Nat.sub_mod_eq_zero_of_mod_eq (Nat.ModEq.pow_card_sub_one_eq_one hp hpn)

Premises used: Nat.sub_mod_eq_zero_of_mod_eq, Nat.ModEq.pow_card_sub_one_eq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a : ℕ
⊢ (1 + p * a) ^ HPow.hPow (β := ℕ) p 0 ≡ 1 [MOD HPow.hPow (β := ℕ) p 0]

Tactic:
Nat.modEq_one

Premises used: Nat.modEq_one, Nat.pow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a : ℕ
⊢ (1 + p * a) ^ HPow.hPow (β := ℕ) p 0 ≡ 1 [MOD HPow.hPow (β := ℕ) p 0]

Tactic:
exact Nat.modEq_one

Premises used: Nat.modEq_one
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ p ^ m ∣ (p * a + 1) ^ p ^ m - 1

Tactic:
rw [Nat.ModEq.comm, add_comm, Nat.modEq_iff_dvd' (Nat.one_le_pow' _ _)] at hm

Premises used: Nat.modEq_iff_dvd', add_comm, Nat.one_le_pow', Nat.ModEq.comm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m : ℕ
hm : p ^ m ∣ (p * a + 1) ^ p ^ m - 1
succ : ∀ (d : ℕ) (hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d), (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]

Tactic:
obtain ⟨d, hd⟩ := hm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
p a m d : ℕ
hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d
⊢ (1 + p * a) ^ p ^ m = p ^ m * d + 1

Tactic:
rw [tsub_eq_iff_eq_add_of_le (Nat.one_le_pow' _ _), add_comm] at hd

Premises used: add_comm, tsub_eq_iff_eq_add_of_le, Nat.one_le_pow'