Commit 2024-04-14 10:41 3bb1d613

View on Github →

chore: remove autoImplicit from more files (#11798) and reduce its scope in a few other instances. Mostly in CategoryTheory and Data this time; some Combinatorics also.

Estimated changes

modified theorem ModuleCat.span_exact
modified def Submodule.torsion'
modified theorem MvPolynomial.algHom_C
modified theorem MvPolynomial.eval_eval₂
modified theorem MvPolynomial.eval₂_id
deleted theorem UnivLE.ofEssSurj.{u,
added theorem UnivLE.ofEssSurj
deleted def UnivLE.witness.{u,
added def UnivLE.witness
deleted theorem UnivLE_iff_essSurj.{u,
added theorem UnivLE_iff_essSurj
modified theorem Prefunctor.mk_map
modified theorem Prefunctor.mk_obj
modified theorem SimpleGraph.Walk.nil_copy
modified def SimpleGraph.Walk.tail
modified def Functor.map_equiv
modified theorem Fin.castPred_le_iff
modified theorem Fin.castPred_lt_iff
modified theorem Fin.castSucc_lt_succ_iff
modified theorem Fin.le_castPred_iff
modified theorem Fin.le_pred_iff
modified theorem Fin.lt_castPred_iff
modified theorem Fin.lt_pred_iff
modified theorem Fin.monotone_castPred_comp
modified theorem Fin.monotone_pred_comp
modified theorem Fin.ofNat'_one
modified theorem Fin.ofNat'_zero
modified theorem Fin.pred_le_iff
modified theorem Fin.pred_lt_castPred
modified theorem Fin.pred_lt_iff
modified theorem Fin.rev_castPred
modified theorem Fin.rev_pred
modified theorem Fin.strictMono_pred_comp
modified theorem Fin.succ_le_castSucc_iff
modified theorem Nat.xgcdAux_succ
modified theorem Nat.xgcdAux_zero
modified theorem List.mapAccumr_eq_foldr
modified theorem List.mapAccumr₂_eq_foldr
modified theorem Nat.binCast_eq
modified theorem Nat.cast_add
modified theorem Nat.cast_bit0
modified theorem Nat.cast_bit1
modified theorem Nat.cast_eq_ofNat
modified theorem Nat.cast_ofNat
modified theorem Nat.cast_one
modified theorem Nat.cast_two
modified theorem one_add_one_eq_two
modified theorem three_add_one_eq_four
modified theorem two_add_one_eq_three
modified theorem Nat.sum_le_ofDigits
modified theorem Nat.ppred_succ
modified theorem Nat.psub_succ
modified theorem Nat.psub_zero
modified theorem Option.elim'_some
modified theorem Prod.mk_inj_left
modified theorem Prod.mk_inj_right
modified theorem Real.lt_sq_of_sqrt_lt
modified theorem Real.sqrt_div
modified theorem Real.sqrt_mul
modified theorem Rel.comp_assoc
modified theorem Set.encard_pair
modified theorem Set.exists_subset_encard_eq
modified theorem Set.ncard_exchange'
modified theorem Set.ncard_exchange
modified theorem Set.ncard_insert_eq_ite
modified theorem Set.ncard_insert_of_mem
modified theorem Set.ncard_insert_of_not_mem
modified theorem Set.ncard_ne_zero_of_mem
modified theorem Set.ncard_pair
modified theorem Set.sep_of_ncard_eq
modified theorem Set.mem_coe_of_mem
modified theorem Set.mem_of_mem_coe
modified theorem EquivLike.range_comp
modified def OrderIso.IciBot
modified def OrderIso.IicTop
modified theorem exists_sUnion
modified theorem forall_sUnion