Theorem: square_eq_two_times (PowerCalc/Examples/Polynomials.lean)

State before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ x ^ 2 = x * x
Tactic:
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]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ x ^ 2 = Monoid.npow (Nat.succ (Nat.succ 0)) x
Tactic:
simp [HPow.hPow, instHPow]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ Monoid.npow (Nat.succ (Nat.succ 0)) x = x * (x * 1)
Tactic:
rw [Monoid.npow_succ, Monoid.npow_succ, Monoid.npow_zero]
State after:
no goals

State before:
R : Type u_1
inst✝ : CommRing R
x : R
⊢ x * (x * 1) = x * x
Tactic:
rw [Monoid.mul_one]
State after:
no goals