Commit 2023-08-27 01:38 6b391efa
View on Github →field_simp: Use positivity as a discharger (#6312)
The main reasons is that having h : 0 < denom
in the context should suffice for field_simp
to do its job, without the need to manually pass h.ne
or similar.
Quite a few have := … ≠ 0
could be dropped, and some field_simp
calls no longer need explicit arguments; this is promising.
This does break some proofs where field_simp
was not used as a closing tactic, and it now
shuffles terms around a bit different. These were fixed. Using field_simp
in the middle of a proof seems rather fragile anyways.
As a drive-by contribution, positivity
now knows about π > 0
.
fixes: #4835