awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
x : R
rw : x ^ HPow.hPow (β := ℕ) p 0 = x
rw₁ : HPow.hPow (β := ℕ) x 1 = x
⊢ (iterateFrobenius R p 0 : (a : R) → R) x = x
have rw₂ : x = x
Tactic: rw [iterateFrobenius_def, pow_zero, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
x : R
⊢ Eq (α := R) ((iterateFrobenius R p (m + n) : (a : R) → R) x : R)
    ((iterateFrobenius R p m : (a : R) → R) ((iterateFrobenius R p n : (a : R) → R) x : R) : R)
have simp_rw : x ^ p ^ (m + n) = (x ^ p ^ n) ^ p ^ m
Tactic: simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
x : R
simp_rw : x ^ p ^ (m + n) = (x ^ p ^ n) ^ p ^ m
⊢ Eq (α := R) ((iterateFrobenius R p (m + n) : (a : R) → R) x : R)
    ((iterateFrobenius R p m : (a : R) → R) ((iterateFrobenius R p n : (a : R) → R) x : R) : R)
have simp_rw₁ : x ^ p ^ (n + m) = (x ^ p ^ n) ^ p ^ m
Tactic: simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
x : R
simp_rw : x ^ p ^ (m + n) = (x ^ p ^ n) ^ p ^ m
simp_rw₁ : x ^ p ^ (n + m) = (x ^ p ^ n) ^ p ^ m
⊢ Eq (α := R) ((iterateFrobenius R p (m + n) : (a : R) → R) x : R)
    ((iterateFrobenius R p m : (a : R) → R) ((iterateFrobenius R p n : (a : R) → R) x : R) : R)
have simp_rw₂ : x ^ (p ^ n * p ^ m) = (x ^ p ^ n) ^ p ^ m
Tactic: simp_rw [iterateFrobenius_def, add_comm m n, pow_add, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p m n : ℕ
inst_1 : ExpChar R p
x : R
⊢ (iterateFrobenius R p (m * n) : (a : R) → R) x = (⇑(iterateFrobenius R p m) : (a : R) → R)^[n] x
have simp_rw : (⇑(frobenius R p) : (a : R) → R)^[m * n] x = (⇑(frobenius R p) : (a : R) → R)^[m]^[n] x
Tactic: simp_rw [coe_iterateFrobenius, Function.iterate_mul]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →* S
g : R →+* S
p m n : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x y : R
inst_4 : Algebra R S
r : R
s : S
⊢ (_root_.frobenius S p : (a : S) → S) (r • s) =
    HSMul.hSMul (α := R) ((_root_.frobenius R p : (a : R) → R) r : R)
      (OneHom.toFun (↑(↑(_root_.frobenius S p) : S →* S) : OneHom S S) s)
have simp_rw : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((_root_.frobenius R p : (a : R) → R) r : R) : S)
    ((_root_.frobenius S p : (a : S) → S) s : S) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) ((_root_.frobenius R p : (a : R) → R) r : R) : S)
    (OneHom.toFun (↑(↑(_root_.frobenius S p) : S →* S) : OneHom S S) s)
Tactic: simp_rw [Algebra.smul_def, map_mul, ← (algebraMap R S).map_frobenius]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Frobenius (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f_1 : R →* S
g : R →+* S
p m n : ℕ
inst_2 : ExpChar R p
inst_3 : ExpChar S p
x y : R
inst_4 : Algebra R S
f : R
s : S
⊢ (_root_.iterateFrobenius S p n : (a : S) → S) (f • s) =
    HSMul.hSMul (α := R) ((_root_.iterateFrobenius R p n : (a : R) → R) f : R)
      (OneHom.toFun (↑(↑(_root_.iterateFrobenius S p n) : S →* S) : OneHom S S) s)
have simp_rw : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (f ^ p ^ n) : S) (s ^ p ^ n) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (f ^ p ^ n) : S)
    (OneHom.toFun (↑(↑(_root_.iterateFrobenius S p n) : S →* S) : OneHom S S) s)
Tactic: simp_rw [iterateFrobenius_def, Algebra.smul_def, mul_pow, ← map_pow]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
t : ℕ
inst_1 : Invertible (α := R) (↑t : R)
inst_2 : Nontrivial R
⊢ ¬ringChar R ∣ t
have rw : Ne.{u_1 + 1} (α := R) (↑t : R) 0
Tactic: rw [← ringChar.spec, ← Ne]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
⊢ HMul.hMul (α := R) (↑n : R) (↑(n.gcdA p) : R) = (↑(n.gcd p) : R)
have suffices : Eq.{u_1 + 1} (α := R) (↑((↑n : ℤ) * n.gcdA p + (↑p : ℤ) * n.gcdB p) : R) (↑(↑(n.gcd p) : ℤ) : R)
Tactic: suffices ↑(n * n.gcdA p + p * n.gcdB p : ℤ) = ((n.gcd p : ℤ) : R) by simpa using this
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (↑((↑n : ℤ) * n.gcdA p + (↑p : ℤ) * n.gcdB p) : R) (↑(↑(n.gcd p) : ℤ) : R)
have rw : Eq.{u_1 + 1} (α := R) (↑(↑(n.gcd p) : ℤ) : R) (↑(↑(n.gcd p) : ℤ) : R)
Tactic: rw [← Nat.gcd_eq_gcd_ab]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
⊢ HMul.hMul (α := R) (↑(n.gcdA p) : R) (↑n : R) = 1
have rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
Tactic: rw [CharP.natCast_gcdA_mul_intCast_eq_gcd, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
⊢ HMul.hMul (α := R) (↑(n.gcdA p) : R) (↑n : R) = 1
have rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
Tactic: rw [CharP.natCast_gcdA_mul_intCast_eq_gcd, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
⊢ HMul.hMul (α := R) (↑(n.gcdA p) : R) (↑n : R) = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [CharP.natCast_gcdA_mul_intCast_eq_gcd, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
⊢ HMul.hMul (α := R) (↑n : R) (↑(n.gcdA p) : R) = 1
have rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
Tactic: rw [CharP.intCast_mul_natCast_gcdA_eq_gcd, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
⊢ HMul.hMul (α := R) (↑n : R) (↑(n.gcdA p) : R) = 1
have rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
Tactic: rw [CharP.intCast_mul_natCast_gcdA_eq_gcd, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
h : n.Coprime p
rw : Eq.{u_1 + 1} (α := R) (↑(n.gcd p) : R) 1
rw₁ : Eq.{u_1 + 1} (α := R) (↑1 : R) 1
⊢ HMul.hMul (α := R) (↑n : R) (↑(n.gcdA p) : R) = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [CharP.intCast_mul_natCast_gcdA_eq_gcd, h, Nat.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (hypothesis)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit.{u_1} (M := R) (↑n : R)
⊢ ¬p ∣ n
have this : Nontrivial R
Tactic: have := CharP.nontrivial_of_char_ne_one (R := R) hp.ne_one
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
n : ℕ
hp : Nat.Prime p
h : IsUnit.{u_1} (M := R) (↑n : R)
this : Nontrivial R
⊢ ¬p ∣ n
have rw : ¬Eq.{u_1 + 1} (α := R) (↑n : R) 0
Tactic: rw [← CharP.cast_eq_zero_iff (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
z : ℤ
hp : Nat.Prime p
⊢ IsUnit.{u_1} (M := R) (↑z : R) ↔ ¬(↑p : ℤ) ∣ z
have inl : ∀ (n : ℕ), IsUnit.{u_1} (M := R) (↑(↑n : ℤ) : R) ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑n : ℤ)
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.CharP.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
p : ℕ
inst_1 : CharP R p
z : ℤ
hp : Nat.Prime p
inl : ∀ (n : ℕ), IsUnit.{u_1} (M := R) (↑(↑n : ℤ) : R) ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑n : ℤ)
⊢ IsUnit.{u_1} (M := R) (↑z : R) ↔ ¬(↑p : ℤ) ∣ z
have inr : ∀ (n : ℕ), IsUnit.{u_1} (M := R) (↑(-(↑n : ℤ)) : R) ↔ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (-(↑n : ℤ))
Tactic: obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ (x + y) ^ p ^ n = ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R)
have rw : Eq.{u_1 + 1} (α := R) (∑ m ∈ range (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
  (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
Tactic: rw [h.add_pow, ← Nat.Ico_zero_eq_range, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R) (∑ m ∈ range (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
    (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
⊢ (x + y) ^ p ^ n = ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R)
have rw₁ : Eq.{u_1 + 1} (α := R) (∑ m ∈ Ico 0 (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
  (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
Tactic: rw [h.add_pow, ← Nat.Ico_zero_eq_range, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R) (∑ m ∈ range (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
    (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
rw₁ :
  Eq.{u_1 + 1} (α := R) (∑ m ∈ Ico 0 (p ^ n + 1), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
    (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
⊢ (x + y) ^ p ^ n = ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R)
have rw₂ : Eq.{u_1 + 1} (α := R) (∑ m ∈ Icc 0 (p ^ n), x ^ m * y ^ (p ^ n - m) * (↑((p ^ n).choose m) : R))
  (∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R))
Tactic: rw [h.add_pow, ← Nat.Ico_zero_eq_range, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ ∑ k ∈ Icc 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R)
have simp_rw : ∑ x_1 ∈ cons (p ^ n) (cons 0 (Ioo 0 (p ^ n)) sorry) sorry, x ^ x_1 * y ^ (p ^ n - x_1) * (↑((p ^ n).choose x_1) : R) =
  x ^ p ^ n + y ^ p ^ n + ∑ x_1 ∈ Ioo 0 (p ^ n), x ^ x_1 * y ^ (p ^ n - x_1) * (↑((p ^ n).choose x_1) : R)
Tactic: simp_rw [Icc_eq_cons_Ico zero_le, Ico_eq_cons_Ioo (pow_pos hp.pos _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : 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))
have simp_rw : x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
  x ^ p ^ n + y ^ p ^ n + ∑ i ∈ Ioo 0 (p ^ n), (↑p : R) * (x ^ i * y ^ (p ^ n - i) * (↑((p ^ n).choose i / p) : R))
Tactic: simp_rw [mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n : ℕ
⊢ x ^ p ^ n + y ^ p ^ n + ∑ k ∈ Ioo 0 (p ^ n), x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ p ^ n + y ^ p ^ n + ∑ i ∈ Ioo 0 (p ^ n), (↑p : R) * (x ^ i * y ^ (p ^ n - i) * (↑((p ^ n).choose i / p) : R))
have h₁ : ∀ (k : ℕ) (hk : k ∈ Ioo 0 (p ^ n)),
  x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    (↑p : R) * (x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))
Tactic: congr! 2 with k hk
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    (↑p : R) * (x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))
have hk₀ : 0 < k
Tactic: obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    (↑p : R) * (x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))
have hk₁ : k < p ^ n
Tactic: obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    (↑p : R) * (x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p) : R))
have h₁ : x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
  x ^ k * y ^ (p ^ n - k) * HMul.hMul (α := R) (↑((p ^ n).choose k / p) : R) (↑p : R)
Tactic: rw [Nat.cast_comm, mul_assoc (_ * _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) =
    x ^ k * y ^ (p ^ n - k) * HMul.hMul (α := R) (↑((p ^ n).choose k / p) : R) (↑p : R)
have h₁ : x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) = x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p * p) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) = x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p * p) : R)
have rw : k ≠ 0
Tactic: rw [Nat.div_mul_cancel (hp.dvd_choose_pow _ _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
rw : k ≠ 0
⊢ x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k) : R) = x ^ k * y ^ (p ^ n - k) * (↑((p ^ n).choose k / p * p) : R)
have rw₁ : k ≠ p ^ n
Tactic: rw [Nat.div_mul_cancel (hp.dvd_choose_pow _ _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
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)
have 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)))
Tactic: rw [h.add_pow_prime_pow_eq' hp, mul_assoc _ x, mul_assoc, mul_sum _ _ (_ * _)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
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)) =
    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)))
have 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))
Tactic: congr! 3 with k hk
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n 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))
have hk₀ : 0 < k
Tactic: obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
n k : ℕ
hk : k ∈ Ioo 0 (p ^ n)
hk₀ : 0 < k
⊢ 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))
have hk₁ : k < p ^ n
Tactic: obtain ⟨hk₀, hk⟩ := mem_Ioo.1 hk
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ 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))
have 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))
Tactic: rw [← mul_pow_sub_one (by lia), ← mul_pow_sub_one (n := p ^ n - k) (by lia)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ 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))
have 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))
Tactic: rw [(h.pow_left _).mul_mul_mul_comm, mul_assoc (x * y)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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))
⊢ 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))
have 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))
Tactic: rw [(h.pow_left _).mul_mul_mul_comm, mul_assoc (x * y)]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p
have zero : ∀ [CharZero R], HPow.hPow (β := ℕ) (x + y) 1 = HPow.hPow (β := ℕ) x 1 + HPow.hPow (β := ℕ) y 1
Tactic: obtain _ | hprime := hR
Cleared hypotheses: p, hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ (x + y) ^ p = x ^ p + y ^ p
have prime : ∀ (hprime : Nat.Prime p) [CharP R p], (x + y) ^ p = x ^ p + y ^ p
Tactic: obtain _ | hprime := hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p : ℕ
h : Commute x y
hprime : Nat.Prime p
hchar : CharP R p
⊢ (x + y) ^ p = x ^ p + y ^ p
have prime : ∀ (r : R) (hr : (x + y) ^ p = x ^ p + y ^ p + (↑p : R) * x * y * r), (x + y) ^ p = x ^ p + y ^ p
Tactic: let ⟨r, hr⟩ := h.exists_add_pow_prime_eq hprime
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
have zero : ∀ [CharZero R], (x + y) ^ HPow.hPow (α := ℕ) 1 n = x ^ HPow.hPow (α := ℕ) 1 n + y ^ HPow.hPow (α := ℕ) 1 n
Tactic: obtain _ | hprime := hR
Cleared hypotheses: p, hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
have prime : ∀ (hprime : Nat.Prime p) [CharP R p], (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
Tactic: obtain _ | hprime := hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
have 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
Tactic: let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hprime n
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
have rw : (x + y) ^ n = (x + y) ^ (n % p) * ((x + y) ^ p) ^ (n / p)
Tactic: rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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)
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
have rw₁ : (x + y) ^ n = (x + y) ^ (n % p) * (x + y) ^ (p * (n / p))
Tactic: rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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))
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
have rw₂ : (x + y) ^ n = (x + y) ^ (n % p + p * (n / p))
Tactic: rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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))
⊢ (x + y) ^ n = (x + y) ^ (n % p) * (x ^ p + y ^ p) ^ (n / p)
have rw₃ : (x + y) ^ n = (x + y) ^ n
Tactic: rw [← add_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
p n : ℕ
hR : ExpChar R p
h : Commute x y
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
have rw : (x - y) ^ n = (x - y) ^ (n % p) * ((x - y) ^ p) ^ (n / p)
Tactic: rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]
-- Lean 4 proof step from Mathlib.Algebra.CharP.Lemmas (goal)
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)
⊢ (x - y) ^ n = (x - y) ^ (n % p) * (x ^ p - y ^ p) ^ (n / p)
have rw₁ : (x - y) ^ n = (x - y) ^ (n % p) * (x - y) ^ (p * (n / p))
Tactic: rw [← sub_pow_expChar_of_commute _ h, ← pow_mul, ← pow_add, Nat.mod_add_div]