Theorem: exercise1_4 (LeanCourse/Assignments/Solutions/Solutions1.lean)

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