How to solve MIL 2.1 problem (a + b) * (a - b) = a^2 - b^2?

Stream: new members

[Ian Liu Rodrigues]

I am following the Math in Lean book, and I am stuck in the following problem from https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html#calculating section:

The following exercise is a little more challenging. You can use the theorems listed underneath.

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  sorry

#check pow_two a
#check mul_sub a b c
#check add_mul a b c
#check add_sub a b c
#check sub_sub a b c
#check add_zero a

The instructions say I can use the "theorems listed underneath". Does this mean it is possible to prove the example by only using those theorems? Or can I use other theorems that I already saw in the book, like sub_self?

Below is my attempt so far, and I'm struggling to prove that x - a + a - y = x - y with the provided theorems:

example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  rw [
    add_mul,
    mul_sub,
    mul_sub,
    ← pow_two,
    ← pow_two,
    add_sub,
    mul_comm b a,
    -- Prove that a^2 - a * b + a * b - b^2 = a^2 - b^2
  ]

[Ruben Van de Velde]

I think you can also use the earlier theorems

[Etienne Marion]

This has already been discussed in this thread