Commit 2024-07-01 09:41 a2617108

View on Github →

chore(SetTheory): remove use of autoImplicit (#14299)

Estimated changes

Modified Mathlib/SetTheory/Cardinal/CountableCover.lean

Modified Mathlib/SetTheory/Cardinal/Finite.lean

modified theorem Nat.card_image_le

modified theorem Nat.card_image_of_injOn

modified theorem Nat.card_image_of_injective

modified theorem Nat.card_preimage_of_injOn

modified theorem Nat.card_preimage_of_injective

Modified Mathlib/SetTheory/Cardinal/UnivLE.lean

Modified Mathlib/SetTheory/Game/PGame.lean

modified theorem SetTheory.PGame.Subsequent.moveLeft_mk_left

modified theorem SetTheory.PGame.Subsequent.moveLeft_mk_right

modified theorem SetTheory.PGame.Subsequent.moveRight_mk_left

modified theorem SetTheory.PGame.Subsequent.moveRight_mk_right

modified theorem SetTheory.PGame.bddAbove_range_of_small

modified theorem SetTheory.PGame.bddBelow_range_of_small

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

modified theorem NatOrdinal.toOrdinal_max

modified theorem NatOrdinal.toOrdinal_min