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!).
I believe the starter code for example 2.4.4 would benefit from 2 more focussing dots:
To be clear, the additional dot are before
calcandextra. This makes the code more readable, and the infoview is more relevant to beginners (like me!).