Commit 2023-01-06 22:29 47a1fd99

View on Github →

feat: remove final sorries in positivity tactic (#1375) Per https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Last.20sorries.20in.20mathlib4

Estimated changes