Exercise in 2.01

Stream: new members

[Kaixin Wang]

I'm trying to do this exercise

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  rw[add_mul] --LHS = a*(a-b) + b*(a-b)
  rw[mul_sub, mul_sub] --LHS = (a*a - a*b) + (b*a - b*b)
  rw[mul_comm b a] --(a*a - a*b) + (a*b - b*b)
  rw[pow_two a, pow_two b] --RHS = a*a - b*b
  rw[add_sub] --LHS = a*a - a*b + a*b - b*b



#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

I now need to show a * a - a * b + a * b - b * b = a * a - b * b, but I'm stuck because I can't use add-com and I don't know how to rewrite this to something like a * a + (-a * b) + a * b - b * b. Any advice?

[Etienne Marion]

You can use docs#sub_add_cancel

[Jose A. Alonso]

Kaixin Wang ha dicho:

I'm trying to do this exercise

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  rw[add_mul] --LHS = a*(a-b) + b*(a-b)
  rw[mul_sub, mul_sub] --LHS = (a*a - a*b) + (b*a - b*b)
  rw[mul_comm b a] --(a*a - a*b) + (a*b - b*b)
  rw[pow_two a, pow_two b] --RHS = a*a - b*b
  rw[add_sub] --LHS = a*a - a*b + a*b - b*b



#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

I now need to show a * a - a * b + a * b - b * b = a * a - b * b, but I'm stuck because I can't use add-com and I don't know how to rewrite this to something like a * a + (-a * b) + a * b - b * b. Any advice?

You can see different proofs here