awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
R : Type u_3
inst : Ring R
inst_1 : IsDomain R
p : ℕ
inst_2 : NeZero p
inst_3 : CharP R p
x : ℤ
⊢ ∃ (a : ℕ) (b : ℕ), HPow.hPow (α := R) (β := ℕ) (↑a : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b : R) 2 = (↑x : R)
have this : Fact (Nat.Prime p)
Tactic: haveI := char_is_prime_of_pos R p
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℕ), HPow.hPow (α := R) (β := ℕ) (↑a : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b : R) 2 = (↑x : R)
have 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)
Tactic: obtain ⟨a, b, hab⟩ := ZMod.sq_add_sq p x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
have refine : HPow.hPow (α := R) (β := ℕ) (↑a.val : R) 2 + HPow.hPow (α := R) (β := ℕ) (↑b.val : R) 2 = (↑x : R)
Tactic: refine ⟨a.val, b.val, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
n : ℕ
x : (ZMod n)ˣ
⊢ x ^ φ n = 1
have zero : ∀ (x : (ZMod 0)ˣ), x ^ φ 0 = 1
Tactic: cases n
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
n : ℕ
x : (ZMod n)ˣ
zero : ∀ (x : (ZMod 0)ˣ), x ^ φ 0 = 1
⊢ x ^ φ n = 1
have succ : ∀ (n : ℕ) (x : (ZMod (n + 1))ˣ), x ^ φ (n + 1) = 1
Tactic: cases n
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
x : (ZMod 0)ˣ
⊢ x ^ φ 0 = 1
have zero : HPow.hPow (β := ℕ) x 0 = 1
Tactic: rw [Nat.totient_zero, pow_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
x : (ZMod 0)ˣ
zero : HPow.hPow (β := ℕ) x 0 = 1
⊢ x ^ φ 0 = 1
have zero₁ : Eq (α := (ZMod 0)ˣ) 1 1
Tactic: rw [Nat.totient_zero, pow_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
n : ℕ
x : (ZMod (n + 1))ˣ
⊢ x ^ φ (n + 1) = 1
have succ : x ^ Fintype.card (ZMod (n + 1))ˣ = 1
Tactic: rw [← card_units_eq_totient, pow_card_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
n : ℕ
x : (ZMod (n + 1))ˣ
succ : x ^ Fintype.card (ZMod (n + 1))ˣ = 1
⊢ x ^ φ (n + 1) = 1
have succ₁ : Eq (α := (ZMod (n + 1))ˣ) 1 1
Tactic: rw [← card_units_eq_totient, pow_card_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
x n : ℕ
h : x.Coprime n
⊢ x ^ φ n ≡ 1 [MOD n]
have rw : Eq (α := ZMod n) (↑(x ^ φ n) : ZMod n) (↑1 : ZMod n)
Tactic: rw [← ZMod.natCast_eq_natCast_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
⊢ Eq (α := ZMod n) (↑(x ^ φ n) : ZMod n) (↑1 : ZMod n)
have this : x' ^ φ n = 1
Tactic: have := ZMod.pow_totient x'
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
x n : ℕ
h : x.Coprime n
x' : (ZMod n)ˣ := unitOfCoprime x h
this : x' ^ φ n = 1
⊢ Eq (α := ZMod n) (↑(x ^ φ n) : ZMod n) (↑1 : ZMod n)
have this₁ : (↑(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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ Membership.mem (γ := Subfield (ZMod p)) ⊥ n
have rwa : ∀ (this : Membership.mem (γ := Subfield (ZMod p)) ⊥ (HSMul.hSMul (β := ZMod p) n.val 1)),
  Membership.mem (γ := Subfield (ZMod p)) ⊥ n
Tactic: rwa [natCast_zsmul, Nat.smul_one_eq_cast, ZMod.natCast_zmod_val] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Membership.mem (γ := Subfield (ZMod p)) ⊥ n
have rwa₁ : ∀ (this : Membership.mem (γ := Subfield (ZMod p)) ⊥ (↑n.val : ZMod p)), Membership.mem (γ := Subfield (ZMod p)) ⊥ n
Tactic: rwa [natCast_zsmul, Nat.smul_one_eq_cast, ZMod.natCast_zmod_val] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Membership.mem (γ := Subfield (ZMod p)) ⊥ n
have rwa₂ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
inst_1 : DivisionRing K
inst_2 : CharP K p
⊢ Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ K)) ⊥
have rw : Eq.{u_1 + 1} (α := Subfield K) (Subfield.map (K := ZMod p) (castHom sorry K) ⊤) ⊥
Tactic: rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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) ⊤) ⊥
⊢ Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ K)) ⊥
have rw₁ : Eq.{u_1 + 1} (α := Subfield K) (Subfield.map (K := ZMod p) (castHom sorry K) ⊤) (Subfield.map (K := ZMod p) (castHom sorry K) ⊥)
Tactic: rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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) ⊥)
⊢ Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ K)) ⊥
have rw₂ : ZMod p →+* K
Tactic: rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ K)) ⊥
have rw₃ : Eq.{u_1 + 1} (α := Subfield K) (Subfield.map (K := ZMod p) (castHom sorry K) ⊤) (Subfield.map (K := ZMod p) (castHom sorry K) ⊤)
Tactic: rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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) ⊤)
⊢ Eq.{u_1 + 1} (α := Subfield K) (RingHom.fieldRange (K := ZMod p) (castHom ⋯ K)) ⊥
have rw₄ : Subfield (ZMod p)
Tactic: rw [RingHom.fieldRange_eq_map, ← Subfield.map_bot (K := ZMod p), Subsingleton.elim ⊥]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p = x
have h : x ^ Fintype.card (ZMod p) = x
Tactic: have h := FiniteField.pow_card x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x
have rwa : ∀ (h : x ^ p = x), x ^ p = x
Tactic: rwa [ZMod.card p] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
n : ℕ
x : ZMod p
⊢ x ^ p ^ n = x
have zero : x ^ HPow.hPow (β := ℕ) p 0 = x
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
n : ℕ
x : ZMod p
zero : x ^ HPow.hPow (β := ℕ) p 0 = x
⊢ x ^ p ^ n = x
have succ : ∀ (n : ℕ) (ih : x ^ p ^ n = x), x ^ p ^ (n + 1) = x
Tactic: induction n with
  | zero => simp
  | succ n ih => simp [pow_succ, pow_mul, ih, pow_card]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p →+* ZMod p) (frobenius (ZMod p) p) (RingHom.id (ZMod p))
have 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)
Tactic: ext a
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
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)
have a₁ : a ^ p = (RingHom.id (ZMod p) : (a : ZMod p) → ZMod p) a
Tactic: rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
a₁ : a ^ p = (RingHom.id (ZMod p) : (a : ZMod p) → ZMod p) 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)
have a₂ : a = (RingHom.id (ZMod p) : (a : ZMod p) → ZMod p) a
Tactic: rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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)
have a₃ : a = a
Tactic: rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Fintype.card (ZMod p)ˣ = p - 1
have rw : Fintype.card (ZMod p) - 1 = p - 1
Tactic: rw [Fintype.card_units, card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Fintype.card (ZMod p) - 1 = p - 1
⊢ Fintype.card (ZMod p)ˣ = p - 1
have rw₁ : p - 1 = p - 1
Tactic: rw [Fintype.card_units, card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : (ZMod p)ˣ
⊢ a ^ (p - 1) = 1
have rw : a ^ Fintype.card (ZMod p)ˣ = 1
Tactic: rw [← card_units p, pow_card_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : (ZMod p)ˣ
rw : a ^ Fintype.card (ZMod p)ˣ = 1
⊢ a ^ (p - 1) = 1
have rw₁ : Eq (α := (ZMod p)ˣ) 1 1
Tactic: rw [← card_units p, pow_card_eq_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p - 1) = 1
have h : a ^ (Fintype.card (ZMod p) - 1) = 1
Tactic: have h := FiniteField.pow_card_sub_one_eq_one a ha
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
h : a ^ (Fintype.card (ZMod p) - 1) = 1
⊢ a ^ (p - 1) = 1
have rwa : ∀ (h : a ^ (p - 1) = 1), a ^ (p - 1) = 1
Tactic: rwa [ZMod.card p] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
⊢ a ^ (p - 1) = if a ≠ 0 then 1 else 0
have pos : ∀ (ha : a ≠ 0), a ^ (p - 1) = 1
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
pos : ∀ (ha : a ≠ 0), a ^ (p - 1) = 1
⊢ a ^ (p - 1) = if a ≠ 0 then 1 else 0
have neg : ∀ (ha : ¬a ≠ 0), a ^ (p - 1) = 0
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f : (ZMod p)[X]
⊢ (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) f = f ^ p
have h : (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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ (expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) f = f ^ p
have 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
Tactic: rwa [ZMod.card p] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
⊢ n ^ (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]
have this : Fact (Nat.Prime p)
Tactic: haveI : Fact p.Prime := ⟨hp⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
this : Fact (Nat.Prime p)
⊢ ¬Eq (α := ZMod p) (↑n : ZMod p) 0
have rw : IsCoprime (↑p : ℤ) n
Tactic: rw [CharP.intCast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n (↑p : ℤ)
this : Fact (Nat.Prime p)
⊢ n ^ (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]
have this₁ : ¬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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p : ℕ
hp : Nat.Prime p
n : ℤ
⊢ n ^ p ≡ n [ZMOD (↑p : ℤ)]
have this : Fact (Nat.Prime p)
Tactic: haveI : Fact p.Prime := ⟨hp⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p x y : ℕ
hp : Nat.Prime p
h : p - 1 ∣ x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have rw : ∀ (h : (p - 1) * ((x - y) / (p - 1)) = x - y) (hxy : y ≤ x) (hy : 0 < y) (n : ℤ), n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
Tactic: rw [← Nat.mul_div_eq_iff_dvd] at h
Cleared hypotheses: h, hxy, hy, n
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have pos : ∀ (hn : n ≡ 0 [ZMOD (↑p : ℤ)]), n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
Tactic: by_cases hn : n ≡ 0 [ZMOD p]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have neg : ∀ (hn : ¬n ≡ 0 [ZMOD (↑p : ℤ)]), n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
Tactic: by_cases hn : n ≡ 0 [ZMOD p]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have pos : HPow.hPow (α := ℤ) 0 x ≡ HPow.hPow (α := ℤ) 0 y [ZMOD (↑p : ℤ)]
Tactic: grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have pos₁ : 0 ≡ HPow.hPow (α := ℤ) 0 y [ZMOD (↑p : ℤ)]
Tactic: grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have pos₂ : 0 ≡ 0 [ZMOD (↑p : ℤ)]
Tactic: grw [hn, zero_pow (hy.trans_le hxy).ne', zero_pow hy.ne']
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have hn₁ : IsCoprime (↑p : ℤ) n
Tactic: rw [Int.modEq_zero_iff_dvd, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have neg : n ^ (x - y) * n ^ y ≡ 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have neg₁ : n ^ ((p - 1) * ((x - y) / (p - 1))) * n ^ y ≡ 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have neg₂ : (n ^ (p - 1)) ^ ((x - y) / (p - 1)) * n ^ y ≡ 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have neg₃ : HPow.hPow (α := ℤ) 1 ((x - y) / (p - 1)) * n ^ y ≡ 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have neg₄ : 1 * n ^ y ≡ 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℤ)]
⊢ n ^ x ≡ n ^ y [ZMOD (↑p : ℤ)]
have neg₅ : n ^ y ≡ 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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p : ℕ
hp : Prime p
n : ℕ
hpn : n.Coprime p
⊢ n ^ (p - 1) ≡ 1 [MOD p]
have rw : HPow.hPow (α := ℤ) (↑n : ℤ) (p - 1) ≡ 1 [ZMOD (↑p : ℤ)]
Tactic: rw [← Int.natCast_modEq_iff, Nat.cast_pow, Nat.cast_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p a m : ℕ
hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
have hm₁ : 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
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p a m : ℕ
hm : p ^ m ∣ (p * a + 1) ^ p ^ m - 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
have succ : ∀ (d : ℕ) (hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d), (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
Tactic: obtain ⟨d, hd⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p a m d : ℕ
hd : (p * a + 1) ^ p ^ m - 1 = p ^ m * d
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
have hd₁ : (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
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
have 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]
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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]
have succ : p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * HPow.hPow (α := ℕ) 1 (p - (k + 1)) * (↑(p.choose (k + 1)) : ℕ)
Tactic: refine Nat.ModEq.add_right 1 (Nat.modEq_zero_iff_dvd.mpr ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p a m d : ℕ
hd : (1 + p * a) ^ p ^ m = p ^ m * d + 1
⊢ p ^ m * p ∣ ∑ k ∈ range p, (p ^ m * d) ^ (k + 1) * HPow.hPow (α := ℕ) 1 (p - (k + 1)) * (↑(p.choose (k + 1)) : ℕ)
have succ : p ^ m * p ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * (↑(p.choose (i + 1)) : ℕ))
Tactic: simp_rw [one_pow, mul_one, pow_succ', mul_assoc, ← Finset.mul_sum]