Commit 2025-10-07 17:36 20bb1bad

View on Github →

chore(Data): golf entire equivFunOnFintype_single, predAbove_right_zero, snoc_zero and more using rfl (#28561)

Estimated changes

Modified Mathlib/Data/DFinsupp/Defs.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Fin/Tuple/Take.lean

Modified Mathlib/Data/Finmap.lean

Modified Mathlib/Data/Finsupp/AList.lean

modified theorem AList.empty_lookupFinsupp

Modified Mathlib/Data/Finsupp/Single.lean

modified theorem Finsupp.zero_update

Modified Mathlib/Data/Matrix/Basic.lean

Modified Mathlib/Data/Matrix/Block.lean

Modified Mathlib/Data/PFunctor/Multivariate/W.lean

Modified Mathlib/Data/PFunctor/Univariate/M.lean

Modified Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean

Modified Mathlib/Data/Seq/Computation.lean

modified theorem Computation.tail_think

Modified Mathlib/Data/Set/Piecewise.lean

Modified Mathlib/Data/Set/Sups.lean

modified theorem Set.image_inf_prod

Modified Mathlib/Data/TypeVec.lean

modified theorem TypeVec.dropFun_diag

Modified Mathlib/Data/Vector/Basic.lean

modified theorem List.Vector.scanl_cons

Modified Mathlib/Data/Vector/Defs.lean

Modified Mathlib/Topology/Connected/PathConnected.lean