Heather Macbeth's course: cancel tactic not working properly

[MajesticGoodness]

Hey, I saw you were working through Heather Macbeth's course. I noticed the cancel tactic wasn't working as expected for you.

I just wanted to let you know that your proof does indeed work! If you just reset the indentation on that line, where you call the cancel, it'll fix it. Indentation is quite finicky in Lean.

example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by
have h3 := 
  calc x * (x + 2) = x ^ 2 + 2 * x := by ring
  _ = 4 + 2 * x := by rw [h1]
  _ = 2 * (x + 2) := by ring 
cancel (x + 2) at h3 -- Reset the indentation on this line.

It kind of goes without saying (but it really should be said) — thanks for curating these awesome courses, and for sharing your learning journey with them. It's hard to shift through all the junk on the 'net, so your resource is invaluable.