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

State before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
x y : R
h : x * y = y * x
⊢ (x + y) * (x + y) = x * x + y * y
Tactic:
rw [add_mul, mul_add, mul_add, ← add_assoc, h, add_add_cancel_right]
State after:
no goals