How are the `_` filled?

Stream: lean4

[Riccardo Brasca]

The following

example : 2 * 3 = 3 * 2 := Nat.add_comm _ _

works. (There are no typos, in the LHS there is multiplication but the proof is Nat.add_comm).

Now, I get that any proof that 6=6 can be put after the :=, but how Lean fill the _'s?

show_term tells me the that the actual proof is

example : 2 * 3 = 3 * 2 := Nat.add_comm (Nat.mul 2 2) 2

And I don't understand why Lean choses 2*2 and 2 and not, for example 1*2 and 4 (that also works). Is it related to how multiplication is actually computed?

[Aaron Liu]

It starts unfolding the multiplication until it exposes addition

[Aaron Liu]

since a.mul b.succ is defeq to a.mul b + b

[Aaron Liu]

try doing set_option trace.Meta.isDefEq true to get some more info

[Riccardo Brasca]

Ah yes of course!

[Kenny Lau]

note that all the basic ways of producing a natural number are all defeq

[Kenny Lau]

that means 3^2-3 and 6*(2-1) and 2*2*2-2 are all defeq to 6

[Ruben Van de Velde]

Yeah, but that wasn't really the question

[Kenny Lau]

well I'd say it's related. The way 2 * 3 got matched with 2*2 + 2 (the left hand sides) is by unfolding; but the way that 3 * 2 also got matched with 2 + 2*2 (the right hand sides) is by the process I described

[Kenny Lau]

another example is:

example : 6 = 6 := Nat.add_comm 5 1

[Riccardo Brasca]

Yeah, you can put after the := literally any proof that 6 = 6. My question was how Lean filled the _, and for some reason I didn't think to definition of multiplication.

[Kevin Buzzard]

example (n : ℕ) : n * 1 = 0 + n := rfl

(but proving that either of them are n is harder)