I managed to have both `H1: V1 & V2 == set0`

and `H2: V1 & V2 != set0`

in my context (with back-quoted, it's a `setI`

), with goal `False`

(`exfalso`

tends to do that), but I don't get how to finish the proof. I thought I could get away with `exact H2 H2`

, but I get issues with `is_true`

...

Either of these should do the trick:

`by rewrite H1 in H2.`

`by case: eqVneq H1 H2.`

BTW, if you want to insert backquotes inside backquoted markdown you only need to add a backquote to the outermost ones, as in ` ``H1 : V1 `&` V2 == set0`` `

@Cyril Cohen excellent, thanks!

Julien Puydt has marked this topic as resolved.

Last updated: Jun 22 2024 at 16:02 UTC