MIL S01_calculating solutions for last questions

Stream: new members

[Kate]

Hi everyone, I am working through MIL, and there are no solutions for the following questions:

-- Try these. For the second, use the theorems listed underneath.
section
variable (a b c d : ℝ)

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by

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

#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

end

While I have completed them, my solutions are far from clean, and I am still getting the hang of everything. Would greatly appreciate a solution that best captures how to execute these questions! Thank you in advance :)

[Julian Berman]

Here's a quick attempt:

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
  rw [add_mul, mul_add, mul_add, add_assoc (a * c + a * d)]

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

I would guess the second one is not what's intended as I don't see sub_self there in the list.

[Kate]

I actually had a similar approach to you and used sub_self as well in the second question. I forgot to add that the book suggests trying 'a more structured calc proof' for the first question too
example : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
and I'm not too sure how to structure that either if you're able to help @Julian Berman.

[Julian Berman]

Here's perhaps something like what's intended:

example : (a + b) * (c + d) = a * c + a * d + b * c + b * d :=
  calc _ = a * (c + d) + b * (c + d) := by rw [add_mul]
       _ = a * c + a * d + b * (c + d) := by rw [mul_add]
       _ = a * c + a * d + (b * c + b * d) := by rw [mul_add]
       _ = a * c + a * d + b * c + b * d := by rw [← add_assoc]

(You'll also eventually learn about the ring tactic which just solves this in one go, I think in the next chapter if not this one.)

[Abraham Solomon]

I don't know about best etc, but this is what i did when i got up to those -- if thats helpful

That chapter is mostly about using rw

section
variable (a b c d : ℝ)

theorem m1 : (a + b) * (c + d) = a * c + a * d + b * c + b * d := by
  rw [mul_add,add_mul,add_mul,←add_assoc,add_assoc (a*c),add_comm (b*c),←add_assoc]

example (a b : ℝ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  have h1: a-b = a+(-b) := rfl;
  rw [h1,m1,mul_neg,mul_neg];
  rw [←pow_two,←pow_two]
  rw [mul_comm b a,add_assoc (a^2),add_comm (-(a*b)),add_neg_cancel,add_zero]
  rfl

[Kate]

Thank you!!