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

State before:
a b : ℝ
⊢ (a + b) * (a - b) = a ^ 2 - b ^ 2
Tactic:
rw [pow_two a]
State after:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b ^ 2

State before:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b ^ 2
Tactic:
rw [pow_two b]
State after:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b * b

State before:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b * b
Tactic:
rw [mul_sub (a+b) a b]
State after:
a b : ℝ
⊢ (a + b) * a - (a + b) * b = a * a - b * b

State before:
a b : ℝ
⊢ (a + b) * a - (a + b) * b = a * a - b * b
Tactic:
rw [add_mul a b a]
State after:
a b : ℝ
⊢ a * a + b * a - (a + b) * b = a * a - b * b

State before:
a b : ℝ
⊢ a * a + b * a - (a + b) * b = a * a - b * b
Tactic:
rw [add_mul a b b]
State after:
a b : ℝ
⊢ a * a + b * a - (a * b + b * b) = a * a - b * b

State before:
a b : ℝ
⊢ a * a + b * a - (a * b + b * b) = a * a - b * b
Tactic:
rw [mul_comm b a]
State after:
a b : ℝ
⊢ a * a + a * b - (a * b + b * b) = a * a - b * b

State before:
a b : ℝ
⊢ a * a + a * b - (a * b + b * b) = a * a - b * b
Tactic:
rw [← sub_sub]
State after:
a b : ℝ
⊢ a * a + a * b - a * b - b * b = a * a - b * b

State before:
a b : ℝ
⊢ a * a + a * b - a * b - b * b = a * a - b * b
Tactic:
rw [← add_sub]
State after:
a b : ℝ
⊢ a * a + (a * b - a * b) - b * b = a * a - b * b

State before:
a b : ℝ
⊢ a * a + (a * b - a * b) - b * b = a * a - b * b
Tactic:
rw [sub_self]
State after:
a b : ℝ
⊢ a * a + 0 - b * b = a * a - b * b

State before:
a b : ℝ
⊢ a * a + 0 - b * b = a * a - b * b
Tactic:
rw [add_zero]
State after:
no goals