which lemmas are used in simple "add 1 to both sides" step

Stream: new members

[rzeta0]

If the following is a hypothesis

$$b-1=0$$

we can use the linarith tactic to derive

$$b=1$$

As a beginner in both lean4 and mathematics itself, I'm interested in which lemmas lean uses to make this step?

By lemmas I mean those things that look like lt_of_ne that I'm only just finding out about.

Is there a debug/verbose mode to ask lean to tell us which lemmas a broad tactic actually used?

Here is a full example that uses this:

example {a b : ℤ} (h1 : a = b + 1) (h2: b - 1 = 0) : a = 2 :=
  have h3: b = 1 := by linarith [h2]
  calc
    a = b + 1 := by rw [h1]
    _ = 1 + 1 := by rw [h3]
    _ = 2 := by norm_num

[Eric Wieser]

You can use show_term to see the very-low-level steps taken by linarith

[jsodd]

By the way, is the output of show_term exactly what lean does?

[jsodd]

If I use show_term intro h, I get "Try this: refine fun h ↦ ?_ h", but it doesn't work...

[Daniel Weber]

linarith is very verbose, in your case you can just use docs#eq_of_sub_eq_zero

[Daniel Weber]

jsodd said:

If I use show_term intro h, I get "Try this: refine fun h ↦ ?_ h", but it doesn't work...

That seems to be a bug, the correct output is simply refine fun h ↦ ?_

[Daniel Weber]

jsodd said:

By the way, is the output of show_term exactly what lean does?

It attempts to be, although sometimes it fails because it's hard to turn parsed expressions back into syntax