When starting a subproof with . the unproven goals warning is not located on the QED, but on the subproof dot. This can look kind of scary, because the warning show the whole state:
Solving this requires some thought about what the most maintainable solution is, it might be more on the Lean side, rather than on the frontend side.
When starting a subproof with . the unproven goals warning is not located on the QED, but on the subproof dot. This can look kind of scary, because the warning show the whole state:
Solving this requires some thought about what the most maintainable solution is, it might be more on the Lean side, rather than on the frontend side.