How to apply Leibniz's law for equality?

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

Apache License 2.0

288 stars 72 forks source link

How to apply Leibniz's law for equality? #103

Open darijgr opened 3 years ago

darijgr commented 3 years ago

How to reduce a goal that says f a = f b to a = b? I'm sure there is a primitive for this, given how fundamental this is. This is worth explaining some time before the Advanced Multiplication boss; it's really useful. lean-1

pasthec commented 3 years ago

It is exactly succ_inj proved in Advanced Addition World, and it is not true for any function f that's why you cannot have a general primitive because it would mean "every function ever is injective".

darijgr commented 3 years ago

No, it's not injectivity. We have a goal of proving f a = f b, and we want to achieve this by proving a = b. The converse would require injectivity.

pasthec commented 3 years ago

Sorry didn't read well, in this case you need the apply tactic