There is a possible bug or inconvenience in level 10 of Advanced Proposition World if you try to solve the different cases by hand instead of using repeat {cc}
The final case which looks like this
P Q : Prop,
p : P,
h : (Q → false) → P → false,
p : ¬P,
q : ¬Q
⊢ Q
cannot be solved since the p : ¬P "hides" p : P.
The way I solved it was by renaming the variables by using by_cases pp : P; by_cases qq : Q, so that the last case looks like this
P Q : Prop,
p : P,
h : (Q → false) → P → false,
pp : ¬P,
qq : ¬Q
⊢ Q
then I just do
have pf :=h(qq),
exfalso,
apply pf,
exact p,
Maybe I am missing something where you can distinguish between terms with the same name but different types by using have or : but I could do not do things like exact p:P or define a new variable with have.
Feel free to close this issue if there is something obvious like that I missed.
There is a possible bug or inconvenience in level 10 of Advanced Proposition World if you try to solve the different cases by hand instead of using
repeat {cc}The final case which looks like this
cannot be solved since the
p : ¬P"hides"p : P.The way I solved it was by renaming the variables by using
by_cases pp : P; by_cases qq : Q,so that the last case looks like thisthen I just do
Maybe I am missing something where you can distinguish between terms with the same name but different types by using
haveor:but I could do not do things likeexact p:Por define a new variable withhave.Feel free to close this issue if there is something obvious like that I missed.