Commit 2024-09-13 03:40 580f59ed

View on Github →

chore: remove autoImplicit from Logic.UnivLE (#16690) Split from #16154.

Estimated changes

Modified Mathlib/Logic/UnivLE.lean

deleted theorem Small.trans_univLE.{u,

added theorem Small.trans_univLE