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

State before:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharTwo R
x y : R
h : x * y = y * x
⊢ (x + y) ^ 2 = x ^ 2 + y ^ 2
Tactic:
rw [sq, sq, sq, add_mul_self_of_Commute h]
State after:
no goals