calc 
x^2 = Monoid.npow (Nat.succ (Nat.succ 0)) x := 
by simp [HPow.hPow, instHPow]
_ = x * (x * 1) := 
by rw [Monoid.npow_succ, Monoid.npow_succ, Monoid.npow_zero]
_ = x * x := by rw [Monoid.mul_one]
R : Type u_1
inst✝ : CommRing R
x : R
⊢ x ^ 2 = x * x
no goals