a stupid question

Stream: lean4

[Hallon]

A stupid question. I am a beginner of Lean.
Why can "rw [pow_two]" be omitted?

Code as follows:
example : x ∣ x ^ 2 := by
-- rw [pow_two]
apply dvd_mul_left

[Mario Carneiro]

because x ^ 2 and x * x are definitionally equal, although this is not obvious

[Mario Carneiro]

x ^ 2
= x * (x ^ 1)
= x * (x * (x ^ 0))
= x * (x * 1)
= x * (x + x * 0)
= x * (x + 0)
= x * x

[Mario Carneiro]

where at each stage I just unfolded the recursive definition of ^, * or +

[Hallon]

I know it is definitional equal. So all equation which is definitonal equal dont need explain?

[Mario Carneiro]

lean will unfold definitions if required to make a theorem application typecheck

[Mario Carneiro]

so yes, in some circumstances

[Hallon]

got. thanks! :grinning:

[Mario Carneiro]

Many tactics like rw are more picky about the form of the input though, which is why theorems like pow_two exist so that you can control what the goal looks like more precisely

[Hallon]

uh-huh

[Hallon]

May I ask where you are from?

[Kevin Buzzard]

normally we stick to Lean questions on this forum

[Yury G. Kudryashov]

You can find Mario's current affiliation at this webpage. Also, his Zulip user profile has geographic coordinates which adds him to this map.