mathlib

da9e1936 - feat(tactic/chain_trans): prove inequalities by transitivity on multiple assumptions