Commit 2024-07-01 17:37 aa30cf90

View on Github →

chore(Order): remove almost all autoImplicit (#14304) In two files, only reduce the scope of it; the other occurrences seem harder to remove.

Estimated changes

Modified Mathlib/Order/Atoms.lean

modified theorem Pi.isAtom_single

modified theorem atom_le_iSup

modified theorem iInf_le_coatom

Modified Mathlib/Order/Bounds/OrderIso.lean

Modified Mathlib/Order/CompleteBooleanAlgebra.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

modified theorem Filter.Tendsto.eventually_forall_ge_atTop

modified theorem Filter.Tendsto.eventually_forall_le_atBot

modified theorem Filter.prod_atBot_atBot_eq

modified theorem Filter.strictMono_subseq_of_tendsto_atTop

modified theorem Filter.tendsto_of_subseq_tendsto

Modified Mathlib/Order/Filter/Bases.lean

Modified Mathlib/Order/Filter/Basic.lean

modified theorem Filter.EventuallyEq.comp_tendsto

modified theorem Filter.filter_injOn_Iic_iff_injOn

modified theorem Filter.frequently_iff_neBot

modified theorem Filter.frequently_mem_iff_neBot

modified theorem Filter.map_mapsTo_Iic_iff_mapsTo

modified theorem Filter.map_surjOn_Iic_iff_surjOn

modified theorem Filter.pure_le_principal

modified theorem GCongr.Filter.comap_le_comap

modified theorem GCongr.Filter.map_le_map

Modified Mathlib/Order/Filter/CountableSeparatingOn.lean

Modified Mathlib/Order/InitialSeg.lean

modified theorem InitialSeg.map_rel_iff

Modified Mathlib/Order/Interval/Finset/Defs.lean

Modified Mathlib/Order/LiminfLimsup.lean

modified theorem Filter.IsBoundedUnder.isCoboundedUnder_flip

Modified Mathlib/Order/Minimal.lean

modified theorem RelEmbedding.inter_preimage_maximals_eq_of_subset

modified theorem RelEmbedding.inter_preimage_minimals_eq_of_subset

modified theorem inter_maximals_preimage_inter_eq_of_rel_iff_rel_on

modified theorem inter_preimage_maximals_eq_of_rel_iff_rel_on_of_subset

modified theorem inter_preimage_minimals_eq_of_rel_iff_rel_on_of_subset

modified theorem mem_maximals_iff_forall_lt_not_mem'

modified theorem mem_maximals_iff_forall_lt_not_mem

modified theorem mem_maximals_iff_forall_ssubset_not_mem

modified theorem mem_maximals_setOf_iff

modified theorem mem_minimals_iff

modified theorem mem_minimals_iff_forall_lt_not_mem'

modified theorem mem_minimals_iff_forall_lt_not_mem

modified theorem mem_minimals_iff_forall_ssubset_not_mem

modified theorem mem_minimals_setOf_iff

Modified Mathlib/Order/RelIso/Basic.lean

modified theorem RelEmbedding.coe_mk

modified theorem RelEmbedding.coe_toEmbedding

modified theorem RelEmbedding.coe_toRelHom