No the definition of == is the regular definition; it's just a deductive reasoning statement. Since the first part of the statement is never true, it doesn't matter what the second part of it says. Of course, like he said, that makes the statement have no value.

> How is it logically coherent?

It's not. But Lean doesn't interrogate logical coherence, just internal consistency.

It is just the definition of "Logical Implication for Material Conditional" and its truth table; see Material Conditional - https://en.wikipedia.org/wiki/Material_conditional

I highly recommend the following two books to study Logic from the beginning (for a layman);

Logic: An Introduction to Elementary Logic by Wilfrid Hodges.

Introduction to Logic: and to the Methodology of Deductive Sciences by Alfred Tarski.

if A then B

Can only be false if there is an instance where A is true, and B is false. In all other cases it's true, even when A is always false.

That's the key.

“if X then Y” means “(not X) or Y”

E.g. “If it’s raining, the sidewalk is wet.” That statement holds if it’s not raining or the sidewalk is wet.

This is a common occurrence in mathematics, where someone might not be able to unconditionally prove Y, but they can under the condition X. Later, another mathematician might build on this by proving X, thereby transitively proving Y. (Or conversely, they might unconditionally disprove Y, thereby disproving X.)

Many hard problems are answered this way.

For example, Fermat’s Last Theorem was proven assuming the Taniyama-Shimura-Weil Conjecture, then Wiles proved the conjecture.

Thousands of theorems rely on the the unproven Reinmann Hypothesis, which is why it’s so interesting to mathematicians.

But if your precondition is “stupid,” your proof is stupid.