Путаница в значении подчеркивания `_` в простом примере Lean

Я учусь использовать помощника по проверке Lean 4. У меня простой вопрос о том, что делает символ подчеркивания _ в следующем контексте:

Следующий пример (src) работает нормально.

example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
  calc
    p = (p - 2 * q) + (2 * q) := by ring
    _ = (1) + (2 * -1) := by rw [h1,h2]
    _ = -1 := by ring

Однако, как новичок, у меня возникает соблазн использовать фактическое имя переменной p в начале каждой строки следующим образом:

example {p q : ℚ} (h1 : p - 2 * q = 1) (h2 : q = -1) : p = -1 :=
  calc
    p = (p - 2 * q) + (2 * q) := by ring
    p = (1) + (2 * -1) := by rw [h1,h2]
    p = -1 := by ring

выдает следующую ошибку:

invalid 'calc' step, left-hand-side is
  p : ℚ
previous right-hand-side is
  p - 2 * q + 2 * q : ℚ

Вопрос: почему это?

Я ожидал, что p = будет действительным и оправданным в качестве начала каждой строки доказательства, и что _ = будет просто сокращением от «предыдущего», во многом так же, как мы пишем доказательство ручкой и бумагой, где мы опускаем левую часть для всех, кроме первой строки.

Очевидно, _ делает что-то, чего я не понимаю и не ожидаю.

Мой анализ

Я не нашел ответа — большинство онлайн-уроков и руководств слишком сложны и предполагают, что мы знаем такие простые вещи.

Моя попытка понять заключается в следующем:

• левая и правая части каждой линии имеют тип Q.
• левая и правая части каждой строки оценивают/упрощают одно и то же выражение, p

так что ошибки быть не должно.