Mop 1.4.7.

Stream: Lean for Scientists and Engineers 2024

[major seitan]

There is a tactic extra in this proof

import Mathlib
--- https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation.html#sq-nonneg
--- 1.4.7. Example
example {m n : ℤ} (h : m ^ 2 + n ≤ 2) : n ≤ 2 :=
  calc
    n = n := by rfl
    _ ≤ m ^ 2 + n := by extra
    _ ≤ 2 := by rel [h]

I might be mistaken but it doesn't seem to be part of mathlib4. If this is the case what is the idiomatic way to work around this?

[Kim Morrison]

Heather's book defines additional tactics. I guess you can use them by adding that repository to your dependencies and importing the relevant file that defines the tactic.

(On mobile, sorry that is rather generic advice!)

[Asei Inoue]

solution in Mathlib

import Mathlib.Tactic

example {m n : ℤ} (h : m ^ 2 + n ≤ 2) : n ≤ 2 :=
  have : m ^ 2 ≥ 0 := by exact sq_nonneg m
  calc
    n = n := by rfl
    _ ≤ m ^ 2 + n := by omega
    _ ≤ 2 := by rel [h]