Commit 2024-03-10 16:40 927ac925

View on Github →

chore: more squeeze_simps arising from linter (#11259) The squeezing continues! All found by the linter at #11246.

Estimated changes

Modified Mathlib/Algebra/Associated.lean

Modified Mathlib/Algebra/Group/Conj.lean

Modified Mathlib/Data/Fin/OrderHom.lean

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/Data/Int/Cast/Prod.lean

Modified Mathlib/Data/List/BigOperators/Basic.lean

Modified Mathlib/Data/List/OfFn.lean

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/List/Permutation.lean

Modified Mathlib/Data/List/Sigma.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Rat/Order.lean

Modified Mathlib/Data/Rel.lean

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/Data/Seq/Parallel.lean

Modified Mathlib/Data/Seq/Seq.lean

Modified Mathlib/Data/Seq/WSeq.lean

modified theorem Stream'.WSeq.join_ret

modified theorem Stream'.WSeq.think_equiv

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

Modified Mathlib/Order/Directed.lean

Modified Mathlib/Order/InitialSeg.lean

Modified Mathlib/Tactic/NormNum/OfScientific.lean