improve example 2.4.4 with focussing dots

[rzeta0]

I believe the starter code for example 2.4.4 would benefit from 2 more focussing dots:

example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a = 0 ∧ b = 0 := by
  have h2 : a ^ 2 = 0
  · apply le_antisymm
    · calc
      a ^ 2 ≤ a ^ 2 + b ^ 2 := by extra
      _ = 0 := by rw [h1]
    · extra
  sorry

To be clear, the additional dot are before calc and extra. This makes the code more readable, and the infoview is more relevant to beginners (like me!).