R : Type u_1
inst✝¹ : Semiring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
R : Type u_1
inst✝¹ : Semiring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
let ⟨r, hr⟩ := h.exists_add_pow_prime_pow_eq hp.out n
no goals
R : Type u_1
inst✝¹ : Semiring R
p n : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
x y : R
h : Commute x y
r : R
hr : (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n + ↑p * r
⊢ (x + y) ^ p ^ n = x ^ p ^ n + y ^ p ^ n
simp [hr]