awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
x x_1 x_2 : Fin n
a : ℕ
isLt : a < n
b : ℕ
isLt_1 : b < n
c : ℕ
isLt_2 : c < n
⊢ a * b * c ≡ a * (b * c) [MOD n]
have rw : a * (b * c) ≡ a * (b * c) [MOD n]
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
x x_1 x_2 : Fin n
a : ℕ
isLt : a < n
b : ℕ
isLt_1 : b < n
c : ℕ
isLt_2 : c < n
⊢ a * (b + c) ≡ a * b + a * c [MOD n]
have rw : a * b + a * c ≡ a * b + a * c [MOD n]
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
a b c : Fin n
⊢ (a + b) * c = a * c + b * c
have rw : c * (a + b) = a * c + b * c
Tactic: rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
a b c : Fin n
rw : c * (a + b) = a * c + b * c
⊢ (a + b) * c = a * c + b * c
have rw₁ : c * a + c * b = a * c + b * c
Tactic: rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
a b c : Fin n
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
⊢ (a + b) * c = a * c + b * c
have rw₂ : c * a + b * c = a * c + b * c
Tactic: rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
a b c : Fin n
rw : c * (a + b) = a * c + b * c
rw₁ : c * a + c * b = a * c + b * c
rw₂ : c * a + b * c = a * c + b * c
⊢ (a + b) * c = a * c + b * c
have rw₃ : a * c + b * c = a * c + b * c
Tactic: rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n
have zero : ∀ [inst : Fintype (ZMod 0)], Fintype.card (ZMod 0) = 0
Tactic: cases n with
  | zero => exact (not_finite (ZMod 0)).elim
  | succ n => convert! Fintype.card_fin (n + 1) using 2
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.ZMod.Defs (goal)
Goal:
n : ℕ
inst : Fintype (ZMod n)
zero : ∀ [inst : Fintype (ZMod 0)], Fintype.card (ZMod 0) = 0
⊢ Fintype.card (ZMod n) = n
have succ : ∀ (n : ℕ) [inst : Fintype (ZMod (n + 1))], Fintype.card (ZMod (n + 1)) = n + 1
Tactic: cases n with
  | zero => exact (not_finite (ZMod 0)).elim
  | succ n => convert! Fintype.card_fin (n + 1) using 2
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
⊢ (↑((p - 1).descFactorial n) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * (↑n ! : ZMod p)
have rw : (↑(∏ i ∈ range n, (p - 1 - i)) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * (↑(∏ i ∈ range n, (i + 1)) : ZMod p)
Tactic: rw [descFactorial_eq_prod_range, factorial_eq_prod_range_add_one]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
⊢ (↑(∏ i ∈ range n, (p - 1 - i)) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * (↑(∏ i ∈ range n, (i + 1)) : ZMod p)
have simp : ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * ∏ i ∈ range n, (↑(i + 1) : ZMod p)
Tactic: simp only [cast_prod]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) n * ∏ i ∈ range n, (↑(i + 1) : ZMod p)
have nth_rw : ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) #(range n) * ∏ i ∈ range n, (↑(i + 1) : ZMod p)
Tactic: nth_rw 2 [← card_range n]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
⊢ ∏ i ∈ range n, (↑(p - 1 - i) : ZMod p) = HPow.hPow (α := ZMod p) (-1) #(range n) * ∏ i ∈ range n, (↑(i + 1) : ZMod p)
have rw : Eq (α := ZMod p) (∏ i ∈ range n, (↑(p - 1 - i) : ZMod p))
  (∏ a ∈ range n, HMul.hMul (α := ZMod p) (-1) (↑(a + 1) : ZMod p))
Tactic: rw [pow_card_mul_prod]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
⊢ Eq (α := ZMod p) (∏ i ∈ range n, (↑(p - 1 - i) : ZMod p))
    (∏ a ∈ range n, HMul.hMul (α := ZMod p) (-1) (↑(a + 1) : ZMod p))
have refine : ∀ x ∈ range n, (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
Tactic: refine prod_congr rfl ?_
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₅ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₅ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₆ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
  HMul.hMul (α := ZMod p) (-1) (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₅ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₆ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    HMul.hMul (α := ZMod p) (-1) (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₇ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
  -HMul.hMul (α := ZMod p) 1 (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₅ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₆ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    HMul.hMul (α := ZMod p) (-1) (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₇ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    -HMul.hMul (α := ZMod p) 1 (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₈ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -(↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₅ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₆ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    HMul.hMul (α := ZMod p) (-1) (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₇ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    -HMul.hMul (α := ZMod p) 1 (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₈ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -(↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₉ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = HAdd.hAdd (α := ZMod p) (-(↑x : ZMod p)) (-1)
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.Factorial (goal)
Goal:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
rw : (↑(p - (x + 1)) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₁ : HSub.hSub (α := ZMod p) (↑p : ZMod p) (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₂ : HSub.hSub (α := ZMod p) 0 (↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₃ : -(↑(x + 1) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
rw₄ : -HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1 = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₅ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -1 * HAdd.hAdd (α := ZMod p) (↑x : ZMod p) 1
rw₆ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    HMul.hMul (α := ZMod p) (-1) (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₇ :
  HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) =
    -HMul.hMul (α := ZMod p) 1 (↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₈ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = -(↑x : ZMod p) + HMul.hMul (α := ZMod p) (-1) 1
rw₉ : HAdd.hAdd (α := ZMod p) (-1) (-(↑x : ZMod p)) = HAdd.hAdd (α := ZMod p) (-(↑x : ZMod p)) (-1)
⊢ (↑(p - 1 - x) : ZMod p) = HMul.hMul (α := ZMod p) (-1) (↑(x + 1) : ZMod p)
have rw₁₀ : HAdd.hAdd (α := ZMod p) (-(↑x : ZMod p)) (-1) = HAdd.hAdd (α := ZMod p) (-(↑x : ZMod p)) (-1)
Tactic: rw [← tsub_add_eq_tsub_tsub_swap,
    Nat.cast_sub <| Nat.le_trans (Nat.add_one_le_iff.mpr (List.mem_range.mp hx)) h,
    CharP.cast_eq_zero, zero_sub, cast_succ, neg_add_rev, mul_add, neg_mul, one_mul,
    mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val ^ z₁.val
have rw : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
Tactic: rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
rw :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val ^ z₁.val
have rw₁ : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val * z₂.val % 2) =
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
Tactic: rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
rw :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val * z₂.val % 2) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val ^ z₁.val
have rw₂ : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val * z₂.val) =
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
Tactic: rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
rw :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val * z₂.val % 2) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
rw₂ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val * z₂.val) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ * z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val ^ z₁.val
have rw₃ : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val) =
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₂.val * z₁.val)
Tactic: rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₁.val *
      HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val
have rw : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
Tactic: rw [← pow_add, ZMod.val_add, ← Int.units_pow_eq_pow_mod_two]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
rw :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₁.val *
      HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val
have rw₁ : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) ((z₁.val + z₂.val) % 2) =
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
Tactic: rw [← pow_add, ZMod.val_add, ← Int.units_pow_eq_pow_mod_two]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
rw :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) ((z₁.val + z₂.val) % 2) =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
⊢ HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁ + z₂).val =
    HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₁.val *
      HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) z₂.val
have rw₂ : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val) =
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) au : ℤˣ) (z₁.val + z₂.val)
Tactic: rw [← pow_add, ZMod.val_add, ← Int.units_pow_eq_pow_mod_two]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul.{u_1, 0, 0} (α := R) (β := Additive ℤˣ) (↑n : R)
        ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ n
have rw : (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
    (HSMul.hSMul (β := Additive ℤˣ) n ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
  u ^ n
Tactic: rw [Nat.cast_smul_eq_nsmul, toMul_nsmul, toMul_ofMul]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
rw :
  (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul (β := Additive ℤˣ) n ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ n
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul.{u_1, 0, 0} (α := R) (β := Additive ℤˣ) (↑n : R)
        ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ n
have rw₁ : HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u) : ℤˣ) n =
  u ^ n
Tactic: rw [Nat.cast_smul_eq_nsmul, toMul_nsmul, toMul_ofMul]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
n : ℕ
rw :
  (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul (β := Additive ℤˣ) n ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ n
rw₁ :
  HPow.hPow (α := ℤˣ) ((Additive.toMul : (a : Additive ℤˣ) → ℤˣ) ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u) : ℤˣ) n =
    u ^ n
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul.{u_1, 0, 0} (α := R) (β := Additive ℤˣ) (↑n : R)
        ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ n
have rw₂ : u ^ n = u ^ n
Tactic: rw [Nat.cast_smul_eq_nsmul, toMul_nsmul, toMul_ofMul]
-- Lean 4 proof step from Mathlib.Data.ZMod.IntUnitsPower (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Module R (Additive ℤˣ)
u : ℤˣ
z : ℤ
⊢ (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
      (HSMul.hSMul.{u_1, 0, 0} (α := R) (β := Additive ℤˣ) (↑z : R)
        ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
    u ^ z
have rw : (Additive.toMul : (a : Additive ℤˣ) → ℤˣ)
    (HSMul.hSMul (β := Additive ℤˣ) z ((Additive.ofMul : (a : ℤˣ) → Additive ℤˣ) u : Additive ℤˣ)) =
  u ^ z
Tactic: rw [Int.cast_smul_eq_zsmul, toMul_zsmul, toMul_ofMul]