awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
rw :
  x ^ p ^ n + y ^ p ^ n +
      HMul.hMul (α := R) (↑p : R) (∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R)) =
    x ^ p ^ n + y ^ p ^ n +
      HMul.hMul (α := R) (↑p : R)
        (∑ i ∈ Ioo 0 (p ^ n), x * y * (x ^ (i - 1) * y ^ (p ^ n - i - 1) * (↑((p ^ n).choose i / p) : R)))
⊢ (x + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n +
      (↑p : R) * x * y * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R)

Tactic:
rw [h.add_pow_prime_pow_eq' hp, mul_assoc _ x, mul_assoc, mul_sum _ _ (_ * _)]

Premises used: Finset.mul_sum, HMul.hMul, mul_assoc, Commute.add_pow_prime_pow_eq'
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
h₁ :
  ∀ (k : ℕ) (hk : k ∈ Ioo 0 (p ^ n)),
    x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R) =
      x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R))
⊢ x ^ p ^ n + y ^ p ^ n +
      HMul.hMul (α := R) (↑p : R) (∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R)) =
    x ^ p ^ n + y ^ p ^ n +
      HMul.hMul (α := R) (↑p : R)
        (∑ i ∈ Ioo 0 (p ^ n), x * y * (x ^ (i - 1) * y ^ (p ^ n - i - 1) * (↑((p ^ n).choose i / p) : R)))

Tactic:
congr! 3 with k hk
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
⊢ p ^ n - k ≠ 0

Tactic:
lia
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
h₁ :
  x * x ^ (k - 1) * (y * y ^ (p ^ n - k - 1)) * (↑((p ^ n).choose k / p) : R) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R))
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R))

Tactic:
rw [← mul_pow_sub_one (by lia), ← mul_pow_sub_one (n := p ^ n - k) (by lia)]

Premises used: mul_pow_sub_one
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk_1 : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
hk : k < p ^ n
h₁ :
  x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1)) * (↑((p ^ n).choose k / p) : R) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R))
h₂ h₃ :
  x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R)) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R))
⊢ x * x ^ (k - 1) * (y * y ^ (p ^ n - k - 1)) * (↑((p ^ n).choose k / p) : R) =
    x * y * (x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R))

Tactic:
rw [(h.pow_left _).mul_mul_mul_comm, mul_assoc (x * y)]

Premises used: Commute.mul_mul_mul_comm, HMul.hMul, mul_assoc, Commute.pow_left
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p =
    x ^ p + y ^ p + HMul.hMul (α := R) (↑p : R) (∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * (↑(p.choose k / p) : R))

Tactic:
simpa using h.add_pow_prime_pow_eq' hp 1

Premises used: OfNat.ofNat, Commute.add_pow_prime_pow_eq'
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p =
    x ^ p + y ^ p + (↑p : R) * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * (↑(p.choose k / p) : R)

Tactic:
simpa using h.add_pow_prime_pow_eq hp 1

Premises used: Commute.add_pow_prime_pow_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∃ (r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + (↑p : R) * x * y * r

Tactic:
⟨_, h.add_pow_prime_pow_eq hp n⟩

Premises used: Commute.add_pow_prime_pow_eq, Exists.intro
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ ∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + (↑p : R) * x * y * r

Tactic:
⟨_, h.add_pow_prime_eq hp⟩

Premises used: Exists.intro, Commute.add_pow_prime_eq
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Nat.Prime p
x y : R
n : ℕ
⊢ (x + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n +
      HMul.hMul (α := R) (↑p : R) (∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))

Tactic:
(Commute.all x y).add_pow_prime_pow_eq' hp n

Premises used: Commute.all, Commute.add_pow_prime_pow_eq'
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Nat.Prime p
x y : R
n : ℕ
⊢ (x + y) ^ p ^ n =
    x ^ p ^ n + y ^ p ^ n +
      (↑p : R) * x * y * ∑ k ∈ Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * (↑((p ^ n).choose k / p) : R)

Tactic:
(Commute.all x y).add_pow_prime_pow_eq hp n

Premises used: Commute.add_pow_prime_pow_eq, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Nat.Prime p
x y : R
⊢ (x + y) ^ p =
    x ^ p + y ^ p + HMul.hMul (α := R) (↑p : R) (∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * (↑(p.choose k / p) : R))

Tactic:
(Commute.all x y).add_pow_prime_eq' hp

Premises used: Commute.add_pow_prime_eq', Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Nat.Prime p
x y : R
⊢ (x + y) ^ p =
    x ^ p + y ^ p + (↑p : R) * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * (↑(p.choose k / p) : R)

Tactic:
(Commute.all x y).add_pow_prime_eq hp

Premises used: Commute.add_pow_prime_eq, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Nat.Prime p
x y : R
n : ℕ
⊢ ∃ (r : R), (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + (↑p : R) * x * y * r

Tactic:
(Commute.all x y).exists_add_pow_prime_pow_eq hp n

Premises used: Commute.exists_add_pow_prime_pow_eq, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
hp : Nat.Prime p
x y : R
⊢ ∃ (r : R), (x + y) ^ p = x ^ p + y ^ p + (↑p : R) * x * y * r

Tactic:
(Commute.all x y).exists_add_pow_prime_eq hp

Premises used: Commute.exists_add_pow_prime_eq, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
zero : ∀ [CharZero R], HPow.hPow (β := ℕ) (x + y) 1 = HPow.hPow (β := ℕ) x 1 + HPow.hPow (β := ℕ) y 1
prime : ∀ (hprime : Nat.Prime p) [CharP R p], (x + y) ^ p = x ^ p + y ^ p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
obtain _ | hprime := hR
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
inst_1 : CharZero R
⊢ HPow.hPow (β := ℕ) (x + y) 1 = HPow.hPow (β := ℕ) x 1 + HPow.hPow (β := ℕ) y 1

Tactic:
simp only [pow_one]

Premises used: pow_one
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar : CharP R p
prime : ∀ (r : R) (hr : (x + y) ^ p = x ^ p + y ^ p + (↑p : R) * x * y * r), (x + y) ^ p = x ^ p + y ^ p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hprime
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar : CharP R p
r : R
hr : (x + y) ^ p = x ^ p + y ^ p + (↑p : R) * x * y * r
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
simp [hr]
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
zero : ∀ [CharZero R], (x + y) ^ HPow.hPow (α := ℕ) 1 n = x ^ HPow.hPow (α := ℕ) 1 n + y ^ HPow.hPow (α := ℕ) 1 n
prime : ∀ (hprime : Nat.Prime p) [CharP R p], (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
obtain _ | hprime := hR
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
h : Commute x y
inst_1 : CharZero R
⊢ (x + y) ^ HPow.hPow (α := ℕ) 1 n = x ^ HPow.hPow (α := ℕ) 1 n + y ^ HPow.hPow (α := ℕ) 1 n

Tactic:
simp only [one_pow, pow_one]

Premises used: one_pow, pow_one
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar : CharP R p
prime :
  ∀ (r : R) (hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + (↑p : R) * x * y * r),
    (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hprime n
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar : CharP R p
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + (↑p : R) * x * y * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
simp [hr]
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
rw : (x + y) ^ n = (x + y) ^ (n % p) * ((x + y) ^ p) ^ (n / p)
rw₁ : (x + y) ^ n = (x + y) ^ (n % p) * (x + y) ^ (p * (n / p))
rw₂ : (x + y) ^ n = (x + y) ^ (n % p + p * (n / p))
rw₃ rw₄ : (x + y) ^ n = (x + y) ^ n
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Tactic:
rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]

Premises used: pow_add, pow_mul, Nat.mod_add_div, add_pow_expChar_of_commute
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
add_pow_expChar_of_commute _ h

Premises used: add_pow_expChar_of_commute
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
add_pow_expChar_pow_of_commute _ _ h

Premises used: add_pow_expChar_pow_of_commute
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Tactic:
add_pow_eq_mul_pow_add_pow_div_expChar_of_commute _ _ h

Premises used: add_pow_eq_mul_pow_add_pow_div_expChar_of_commute
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p : ℕ
hR : ExpChar R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
add_pow_expChar_of_commute _ <| .all ..

Premises used: add_pow_expChar_of_commute, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p n : ℕ
hR : ExpChar R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
add_pow_expChar_pow_of_commute _ _ <| .all ..

Premises used: add_pow_expChar_pow_of_commute, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p n : ℕ
hR : ExpChar R p
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Tactic:
add_pow_eq_mul_pow_add_pow_div_expChar_of_commute _ _ <| .all ..

Premises used: add_pow_eq_mul_pow_add_pow_div_expChar_of_commute, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p

Tactic:
add_pow_expChar ..

Premises used: add_pow_expChar
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p n : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n

Tactic:
add_pow_expChar_pow ..

Premises used: add_pow_expChar_pow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
p n : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)

Tactic:
add_pow_eq_mul_pow_add_pow_div_expChar ..

Premises used: add_pow_eq_mul_pow_add_pow_div_expChar
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p

Tactic:
simp [eq_sub_iff_add_eq, ← add_pow_expChar_of_commute _ (h.sub_left rfl)]

Premises used: eq_sub_iff_add_eq, add_pow_expChar_of_commute, rfl, Commute.sub_left
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

Tactic:
simp [eq_sub_iff_add_eq, ← add_pow_expChar_pow_of_commute _ _ (h.sub_left rfl)]

Premises used: add_pow_expChar_pow_of_commute, eq_sub_iff_add_eq, rfl, Commute.sub_left
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
rw : (x - y) ^ n = (x - y) ^ (n % p) * ((x - y) ^ p) ^ (n / p)
rw₁ : (x - y) ^ n = (x - y) ^ (n % p) * (x - y) ^ (p * (n / p))
rw₂ : (x - y) ^ n = (x - y) ^ (n % p + p * (n / p))
rw₃ rw₄ : (x - y) ^ n = (x - y) ^ n
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Tactic:
rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]

Premises used: sub_pow_expChar_of_commute, pow_add, pow_mul, Nat.mod_add_div
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
rw : HPow.hPow (α := R) (-1) p + 1 = 0
⊢ HPow.hPow (α := R) (-1) p = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
nth_rw : HPow.hPow (α := R) (-1) p + HPow.hPow (α := R) 1 p = 0
⊢ HPow.hPow (α := R) (-1) p + 1 = 0

Tactic:
nth_rw 2 [← one_pow p]

Premises used: one_pow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hR : ExpChar R p
rw : HAdd.hAdd (α := R) (-1) 1 ^ p = 0
rw₁ : HPow.hPow (α := R) 0 p = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) (-1) p + HPow.hPow (α := R) 1 p = 0

Tactic:
rw [← add_pow_expChar_of_commute _ (Commute.one_right _), neg_add_cancel,
    zero_pow (expChar_ne_zero R p)]

Premises used: neg_add_cancel, add_pow_expChar_of_commute, expChar_ne_zero, zero_pow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
rw : HPow.hPow (α := R) (-1) (p ^ n) + 1 = 0
⊢ HPow.hPow (α := R) (-1) (p ^ n) = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
nth_rw : HPow.hPow (α := R) (-1) (p ^ n) + HPow.hPow (α := R) 1 (p ^ n) = 0
⊢ HPow.hPow (α := R) (-1) (p ^ n) + 1 = 0

Tactic:
nth_rw 2 [← one_pow (p ^ n)]

Premises used: one_pow, HPow.hPow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hR : ExpChar R p
rw : HAdd.hAdd (α := R) (-1) 1 ^ p ^ n = 0
rw₁ : HPow.hPow (α := R) 0 (p ^ n) = 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) (-1) (p ^ n) + HPow.hPow (α := R) 1 (p ^ n) = 0

Tactic:
rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
    zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]

Premises used: add_pow_expChar_pow_of_commute, pow_ne_zero, neg_add_cancel, expChar_ne_zero, zero_pow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
x y : R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Commute x y
⊢ (x - y) ^ p = x ^ p - y ^ p

Tactic:
sub_pow_expChar_of_commute _ h

Premises used: sub_pow_expChar_of_commute
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
x y : R
p n : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Commute x y
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

Tactic:
sub_pow_expChar_pow_of_commute _ _ h

Premises used: sub_pow_expChar_pow_of_commute
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ HPow.hPow (α := R) (-1) p = -1

Tactic:
neg_one_pow_expChar ..

Premises used: neg_one_pow_expChar
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ HPow.hPow (α := R) (-1) (p ^ n) = -1

Tactic:
neg_one_pow_expChar_pow ..

Premises used: neg_one_pow_expChar_pow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
x y : R
p n : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Tactic:
sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute _ _ h

Premises used: sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
hR : ExpChar R p
⊢ (x - y) ^ p = x ^ p - y ^ p

Tactic:
sub_pow_expChar_of_commute _ <| .all ..

Premises used: sub_pow_expChar_of_commute, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
n p : ℕ
hR : ExpChar R p
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

Tactic:
sub_pow_expChar_pow_of_commute _ _ <| .all ..

Premises used: sub_pow_expChar_pow_of_commute, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
n p : ℕ
hR : ExpChar R p
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Tactic:
sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute _ _ <| .all ..

Premises used: sub_pow_eq_mul_pow_sub_pow_div_expChar_of_commute, Commute.all
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ (x - y) ^ p = x ^ p - y ^ p

Tactic:
sub_pow_expChar ..

Premises used: sub_pow_expChar
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
n p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ (x - y) ^ p ^ n = x ^ p ^ n - y ^ p ^ n

Tactic:
sub_pow_expChar_pow ..

Premises used: sub_pow_expChar_pow
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
n p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R p
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)

Tactic:
sub_pow_eq_mul_pow_sub_pow_div_expChar ..

Premises used: sub_pow_eq_mul_pow_sub_pow_div_expChar
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ (↑p : R) * x
rw : r ∣ x ^ p + (↑p : R) * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * (↑(p.choose k / p) : R)
⊢ r ∣ (x + y) ^ p - y ^ p

Tactic:
rw [add_pow_prime_eq hpri, add_right_comm, add_assoc, add_sub_assoc, add_sub_cancel_right]

Premises used: add_sub_assoc, add_assoc, add_right_comm, add_pow_prime_eq, add_sub_cancel_right
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ (↑p : R) * x
⊢ r ∣ x ^ p + (↑p : R) * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * (↑(p.choose k / p) : R)

Tactic:
dvd_add h₁ (h₂.trans <| (dvd_mul_right ..).trans <| dvd_mul_right ..)

Premises used: dvd_mul_right, dvd_add, Dvd.dvd.trans
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : CommRing R
x y : R
p : ℕ
hpri : Prime p
r : R
h₁ : r ∣ x ^ p
h₂ : r ∣ (↑p : R) * x
⊢ r ∣ x ^ p + (↑p : R) * x * y * ∑ k ∈ Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * (↑(p.choose k / p) : R)

Tactic:
exact dvd_add h₁ (h₂.trans <| (dvd_mul_right ..).trans <| dvd_mul_right ..)

Premises used: dvd_mul_right, dvd_add, Dvd.dvd.trans
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Finite R
inst_2 : CharP R 0
⊢ CharZero R

Tactic:
haveI : CharZero R := charP_to_charZero R
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Finite R
inst_2 : CharP R 0
this : CharZero R
⊢ False

Tactic:
absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))

Premises used: not_injective_infinite_finite, Nat.cast, absurd, Nat.cast_injective
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Finite R
inst_2 : CharP R 0
this : CharZero R
⊢ False

Tactic:
exact absurd Nat.cast_injective (not_injective_infinite_finite ((↑) : ℕ → R))

Premises used: not_injective_infinite_finite, Nat.cast, absurd, Nat.cast_injective
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : NonAssocRing R
inst_1 : Finite R
⊢ ringChar R ≠ 0

Tactic:
char_ne_zero_of_finite R (ringChar R)

Premises used: ringChar, CharP.char_ne_zero_of_finite
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
inst_3 : Finite R
p : ℕ
inst_4 : CharP R p
⊢ Nat.Prime p

Tactic:
Or.resolve_right (char_is_prime_or_zero R p) (char_ne_zero_of_finite R p)

Premises used: CharP.char_is_prime_or_zero, CharP.char_ne_zero_of_finite, Or.resolve_right
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
inst_3 : Finite R
apply : ringChar R ≠ 0
⊢ Nat.Prime (ringChar R)

Tactic:
apply CharP.char_prime_of_ne_zero R

Premises used: CharP.char_prime_of_ne_zero
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
inst_3 : Finite R
⊢ ringChar R ≠ 0

Tactic:
CharP.ringChar_ne_zero_of_finite R

Premises used: CharP.ringChar_ne_zero_of_finite
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_1
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
inst_3 : Finite R
⊢ ringChar R ≠ 0

Tactic:
exact CharP.ringChar_ne_zero_of_finite R

Premises used: CharP.ringChar_ne_zero_of_finite
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
l : List R
⊢ l.sum ^ p = List.sum (List.map (fun (x : R) ↦ x ^ p) l)

Tactic:
map_list_sum (frobenius R p) _

Premises used: map_list_sum, frobenius
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
s : Multiset R
⊢ s.sum ^ p = Multiset.sum (Multiset.map (fun (x : R) ↦ x ^ p) s)

Tactic:
map_multiset_sum (frobenius R p) _

Premises used: map_multiset_sum, frobenius
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
ι : Type u_4
s : Finset ι
f : ι → R
⊢ HPow.hPow (α := R) (∑ i ∈ s, f i) p = ∑ i ∈ s, f i ^ p

Tactic:
map_sum (frobenius R p) _ _

Premises used: map_sum, frobenius
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
l : List R
⊢ l.sum ^ p ^ n = List.sum (List.map (fun (x : R) ↦ x ^ p ^ n) l)

Tactic:
map_list_sum (iterateFrobenius R p n) _

Premises used: map_list_sum, iterateFrobenius
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
s : Multiset R
⊢ s.sum ^ p ^ n = Multiset.sum (Multiset.map (fun (x : R) ↦ x ^ p ^ n) s)

Tactic:
map_multiset_sum (iterateFrobenius R p n) _

Premises used: map_multiset_sum, iterateFrobenius
-- Module: Mathlib.Algebra.CharP.Lemmas
Goal:
R : Type u_3
inst : CommSemiring R
p n : ℕ
inst_1 : ExpChar R p
ι : Type u_4
s : Finset ι
f : ι → R
⊢ HPow.hPow (α := R) (∑ i ∈ s, f i) (p ^ n) = ∑ i ∈ s, f i ^ p ^ n

Tactic:
map_sum (iterateFrobenius R p n) _ _

Premises used: map_sum, iterateFrobenius
-- Module: Mathlib.Algebra.CharP.LinearMaps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ (x : M), Eq (α := Ideal R) (Ideal.torsionOf R M x) ⊥
n : ℕ
⊢ (↑n : M →ₗ[R] M) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) 1

Tactic:
simp only [Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]

Premises used: Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one
-- Module: Mathlib.Algebra.CharP.LinearMaps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : ℕ
hchar : CharP R p
htorsion : ∃ (x : M), Eq (α := Ideal R) (Ideal.torsionOf R M x) ⊥
n : ℕ
⊢ (↑n : M →ₗ[R] M) = HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M →ₗ[R] M) (↑n : R) 1

Tactic:
have exact : (n : M →ₗ[R] M) = (n : R) • 1 := by
      simp only [Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]