Theorem: LoVe.ring_example (LoVe/Lectures/LoVe13_BasicMathematicalStructures_Demo.lean)

State before:
a b : Int2
⊢ (a + b) ^ 3 = a ^ 3 + 3 * a ^ 2 * b + 3 * a * b ^ 2 + b ^ 3
Tactic:
ring
State after:
no goals