Theorem: IMOSL.Extra.CharTwo.add_one_mul_self (IMOSLLean4/Extra/CharTwo/Ring/Basic.lean)

State before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
x : R
⊢ (x + 1) * (x + 1) = x * x + 1
Tactic:
rw [add_mul_self_of_Commute ((mul_one x).trans (one_mul x).symm), one_mul]
State after:
no goals