awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∣ p ^ m * (d * ∑ i ∈ range p, (p ^ m * d) ^ i * (↑(p.choose (i + 1)) : ℕ))
have succ : ∀ (k : ℕ) (hk : k ∈ range p), p ∣ (p ^ m * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
Tactic: refine mul_dvd_mul_left (p ^ m) (dvd_mul_of_dvd_right (Finset.dvd_sum fun k hk ↦ ?_) d)
-- 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
k : ℕ
hk : k ∈ range p
⊢ p ∣ (p ^ m * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
have 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)) : ℕ)
Tactic: cases m
Cleared hypotheses: m, 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
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)) : ℕ)
⊢ p ∣ (p ^ m * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
have succ₁ : ∀ (n : ℕ) (hd : (1 + p * a) ^ p ^ (n + 1) = p ^ (n + 1) * d + 1), p ∣ (p ^ (n + 1) * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
Tactic: cases m
Cleared hypotheses: m, hd
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
p a d k : ℕ
hk : k ∈ range p
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)) : ℕ)
have hd₁ : p * a = d
Tactic: rw [pow_zero, pow_one, one_mul, add_comm, add_left_inj] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p a d k : ℕ
hk : k ∈ range p
hd : p * a = d
⊢ p ∣ (HPow.hPow (β := ℕ) p 0 * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
have succ : ∀ (hk : 0 ∈ range p), p ∣ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) p 0 * d) 0 * (↑(p.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℕ)
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)) : ℕ)
⊢ p ∣ (HPow.hPow (β := ℕ) p 0 * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
have succ₁ : ∀ (n : ℕ) (hk : n + 1 ∈ range p), p ∣ (HPow.hPow (β := ℕ) p 0 * d) ^ (n + 1) * (↑(p.choose (n + 1 + 1)) : ℕ)
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p a d k : ℕ
hk : k ∈ range p
n : ℕ
hd : (1 + p * a) ^ p ^ (n + 1) = p ^ (n + 1) * d + 1
⊢ p ∣ (p ^ (n + 1) * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
have succ : ∀ (hk : 0 ∈ range p), p ∣ HPow.hPow (β := ℕ) (p ^ (n + 1) * d) 0 * (↑(p.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℕ)
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)) : ℕ)
⊢ p ∣ (p ^ (n + 1) * d) ^ k * (↑(p.choose (k + 1)) : ℕ)
have succ₁ : ∀ (n_1 : ℕ) (hk : n_1 + 1 ∈ range p), p ∣ (p ^ (n + 1) * d) ^ (n_1 + 1) * (↑(p.choose (n_1 + 1 + 1)) : ℕ)
Tactic: cases k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p m a : ℕ
⊢ (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
have zero : (1 + p * a) ^ HPow.hPow (β := ℕ) p 0 ≡ 1 [MOD HPow.hPow (β := ℕ) p 0]
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']
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
p m a : ℕ
zero : (1 + p * a) ^ HPow.hPow (β := ℕ) p 0 ≡ 1 [MOD HPow.hPow (β := ℕ) p 0]
⊢ (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]
have succ : ∀ (m : ℕ) (hm : (1 + p * a) ^ p ^ m ≡ 1 [MOD p ^ m]), (1 + p * a) ^ p ^ (m + 1) ≡ 1 [MOD p ^ (m + 1)]
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']
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
⊢ a = 1 ∨ IsUnit (a - 1)
have inl : ∀ (hn : 0 = p ^ k) (a : ZMod 0) (ha : (orderOf a).Coprime 0), a = 1 ∨ IsUnit (a - 1)
Tactic: rcases eq_or_ne n 0 with rfl | hn0
Cleared hypotheses: n, hn, a, ha
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ a = 1 ∨ IsUnit (a - 1)
have inr : ∀ (hn0 : n ≠ 0), a = 1 ∨ IsUnit (a - 1)
Tactic: rcases eq_or_ne n 0 with rfl | hn0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
n p k : ℕ
inst : Fact (Nat.Prime p)
hn : n = p ^ k
a : ZMod n
ha : (orderOf a).Coprime n
hn0 : n ≠ 0
⊢ a = 1 ∨ IsUnit (a - 1)
have inr : ∀ (ha : (orderOf (G := ZMod n) 0).Coprime n), Eq (α := ZMod n) 0 1 ∨ IsUnit (HSub.hSub (α := ZMod n) 0 1)
Tactic: rcases eq_or_ne a 0 with rfl | ha0
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ a = 1 ∨ IsUnit (a - 1)
have inr₁ : ∀ (ha0 : a ≠ 0), a = 1 ∨ IsUnit (a - 1)
Tactic: rcases eq_or_ne a 0 with rfl | ha0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ a = 1 ∨ IsUnit (a - 1)
have this : NeZero n
Tactic: have : NeZero n := ⟨hn0⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ a = 1 ∨ IsUnit (a - 1)
have 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)
Tactic: obtain ⟨a, rfl⟩ := ZMod.natCast_zmod_surjective a
Cleared hypotheses: a, ha, ha0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq (α := ZMod n) (↑a : ZMod n) 1 ∨ IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)
have inr : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1) → orderOf (G := ZMod n) (↑a : ZMod n) = 1
Tactic: rw [← orderOf_eq_one_iff, or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
have inr : ∀ (h : ¬IsUnit (HSub.hSub (α := ZMod n) (↑a : ZMod n) 1)), orderOf (G := ZMod n) (↑a : ZMod n) ∣ n
Tactic: refine fun h ↦ ha.eq_one_of_dvd ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ orderOf (G := ZMod n) (↑a : ZMod n) ∣ n
have inr : a ^ p ^ k ≡ 1 [MOD p ^ k]
Tactic: rw [orderOf_dvd_iff_pow_eq_one, ← Nat.cast_pow, ← Nat.cast_one, ZMod.natCast_eq_natCast_iff, hn]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
have contrapose! : ∀ (ha0 : a < 1), Eq (α := ZMod n) (↑a : ZMod n) 0
Tactic: contrapose! ha0
Cleared hypotheses: ha0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq (α := ZMod n) (↑a : ZMod n) 0
have rw : Eq (α := ZMod n) (↑0 : ZMod n) 0
Tactic: rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq (α := ZMod n) (↑a : ZMod n) 0
have rw₁ : Eq (α := ZMod n) 0 0
Tactic: rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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)
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]
have ha0₁ : 1 ≤ a
Tactic: replace ha0 : 1 ≤ a := by
    contrapose! ha0
    rw [Nat.lt_one_iff.mp ha0, Nat.cast_zero]
Cleared hypotheses: ha0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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 ^ p ^ k ≡ 1 [MOD p ^ k]
have h₁ : ¬(a - 1).Coprime (p ^ k)
Tactic: rw [← Nat.cast_one, ← Nat.cast_sub ha0, ZMod.isUnit_iff_coprime, hn] at h
Cleared hypotheses: h, ha0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ a ^ p ^ k ≡ 1 [MOD p ^ k]
have inr : ∀ (b : ℕ) (hb : a - 1 = p * b), 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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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]
have hb₁ : a = 1 + p * b
Tactic: rw [tsub_eq_iff_eq_add_of_le ha0, add_comm] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
⊢ Nat.card.{u_3} ↥⊥ = p
have rw : Nat.card.{u_3} ↥(RingHom.fieldRange (K := ZMod p) (castHom sorry F)) = p
Tactic: rw [← fieldRange_castHom_eq_bot p,
    ← Nat.card_eq_of_bijective _ (RingHom.rangeRestrictField_bijective _), Nat.card_zmod]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Nat.card.{u_3} ↥⊥ = p
have rw₁ : Nat.card (ZMod p) = p
Tactic: rw [← fieldRange_castHom_eq_bot p,
    ← Nat.card_eq_of_bijective _ (RingHom.rangeRestrictField_bijective _), Nat.card_zmod]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Nat.card.{u_3} ↥⊥ = p
have rw₂ : p = p
Tactic: rw [← fieldRange_castHom_eq_bot p,
    ← Nat.card_eq_of_bijective _ (RingHom.rangeRestrictField_bijective _), Nat.card_zmod]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ x ∈ Finset.map { toFun := (⇑(castHom ⋯ F) : (a : ZMod p) → F), inj' := ⋯ : ZMod p ↪ F } univ ↔
    Membership.mem (γ := Subfield F) ⊥ x
have simp_rw : (∃ (a : ZMod p), ({ toFun := (⇑(castHom sorry F) : (a : ZMod p) → F), inj' := sorry : ZMod p ↪ F } : (a : ZMod p) → F) a = x) ↔
  Membership.mem (γ := Subfield F) (RingHom.fieldRange (K := ZMod p) (castHom sorry F)) x
Tactic: simp_rw [Finset.mem_map, mem_univ, true_and, ← fieldRange_castHom_eq_bot p]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 p - X).roots
have rw : (HPow.hPow (α := (↥⊥)[X]) X (Fintype.card.{u_3} ↥⊥) - X).roots
Tactic: rw [← card_bot F p, ← Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 p - X).roots = Finset.val univ
have conv_lhs : (HPow.hPow (α := (↥⊥)[X]) X (Fintype.card.{u_3} ↥⊥) - X).roots = Finset.val univ
Tactic: conv_lhs => rw [← card_bot F p, ← Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 p - X).Splits
have rw : (HPow.hPow (α := (↥⊥)[X]) X p - X).roots.card = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).Splits
have rw₁ : Multiset.card.{u_3} (α := ↥⊥) (Finset.val univ) = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).Splits
have rw₂ : Finset.card.{u_3} (α := ↥⊥) univ = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).Splits
have rw₃ : Fintype.card.{u_3} ↥⊥ = (HPow.hPow (α := (↥⊥)[X]) X p - X).natDegree
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).Splits
have rw₄ : Fintype.card.{u_3} ↥⊥ = p
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).Splits
have rw₅ : Nat.card.{u_3} ↥⊥ = p
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ (HPow.hPow (α := (↥⊥)[X]) X p - X).Splits
have rw₆ : p = p
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
F : Type u_3
inst : Field F
p : ℕ
inst_1 : Fact (Nat.Prime p)
inst_2 : CharP F p
x : F
⊢ Membership.mem (γ := Subfield F) ⊥ x ↔ x ^ p = x
have 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
Tactic: have := roots_X_pow_char_sub_X_bot F p ▸
      (splits_bot F p).roots_map (Subfield.subtype _) ▸ Multiset.mem_map (b := x)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
F : Type u_3
inst : Field F
inst_1 : Finite F
hF : ringChar F ≠ 2
⊢ ∃ (a : F), ¬IsSquare a
have h : ¬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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
⊢ ringChar F = 2 ↔ Fintype.card F % 2 = 0
have rcases : ∀ (n : ℕ+) (hp : Nat.Prime (ringChar F)) (h : Fintype.card F = ringChar F ^ (↑n : ℕ)),
  ringChar F = 2 ↔ Fintype.card F % 2 = 0
Tactic: rcases FiniteField.card F (ringChar F) with ⟨n, hp, h⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 ↔ Fintype.card F % 2 = 0
have rw : ringChar F = 2 ↔ ringChar F = 2 ∧ (↑n : ℕ) ≠ 0
Tactic: rw [h, ← Nat.even_iff, Nat.even_pow, hp.even_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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 / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
have h₁ : a ^ (Fintype.card F - 1) = 1
Tactic: have h₁ := FiniteField.pow_card_sub_one_eq_one a ha
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
have h₂ : a ^ (Fintype.card F / 2) * a ^ (Fintype.card F / 2) = 1
Tactic: rw [← Nat.two_mul_odd_div_two (FiniteField.odd_card_of_char_ne_two hF), mul_comm, pow_mul,
    pow_two] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a : Fˣ
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have obtain : ∀ (g : Fˣ) (hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x),
  IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
Tactic: obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := Fˣ)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
⊢ Membership.mem (γ := Submonoid Fˣ) (Submonoid.powers g) a
have rw : Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) a
Tactic: rw [mem_powers_iff_mem_zpowers]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
F : Type u_3
inst : Field F
inst_1 : Fintype F
hF : ringChar F ≠ 2
a g : Fˣ
hg : ∀ (x : Fˣ), Membership.mem (γ := Subgroup Fˣ) (Subgroup.zpowers g) x
⊢ IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
have obtain : ∀ (n : ℕ) (hn : (fun (x : ℕ) ↦ g ^ x) n = a), IsSquare a ↔ a ^ (Fintype.card F / 2) = 1
Tactic: obtain ⟨n, hn⟩ : a ∈ Submonoid.powers g := by rw [mem_powers_iff_mem_zpowers]; apply hg