MoP 1.2.4

Stream: Lean for Scientists and Engineers 2024

[Tyler Josephson ⚛️]

Illustrating how to ask Lean questions on Zulip

[Tyler Josephson ⚛️]

#mwe and #backticks

[Tyler Josephson ⚛️]

import Mathlib

example {a b c d e f : ℤ} (h1 : a * d = b * c) (h2 : c * f = d * e) :
    d * (a * f - b * e) = 0 :=
  calc
    d * (a * f - b * e) = (a * d) * f - b * d * e := by ring
    _ = (b * c) * f - b * (c * f) := by rw [h1,h2]
    _ = 0 := by ring

This is having a problem with the rw line

[Tyler Josephson ⚛️]

Gonzalo saw the issue, the parentheses should be d * (a * f - b * e) = (a*d)*f-(d*e)*b