Commit 2025-06-27 12:16 cf17ac4e

View on Github →

chore: remove unused simp arguments (#26430) This removes unused simp arguments flagged by Lean's new linter.unusedSimpArgs. This branch was created on nightly-testing, where we have the linter, and then rebased onto master, resolving all merge conflicts to master’s code, so some might be left. I used a python script to remove the reported simp arguments, and then manually fixed the breakage (mostly changing ← foo to - foo instead of removing it when needed).

Estimated changes

modified theorem geom_sum_one
modified theorem mul_left_iterate_apply_one
modified theorem Polynomial.comp_C
modified theorem mem_sphere_one_iff_norm
modified theorem ball_one_mul_singleton
modified theorem Composition.boundary_zero
modified theorem guard_true
modified theorem Complex.cos_neg
modified theorem Complex.sinh_neg
modified theorem Real.cos_neg
modified theorem Real.sin_neg
modified theorem Real.sinh_neg
modified theorem Real.tan_neg
modified theorem Real.tanh_neg
modified theorem List.rdropWhile_nil
modified theorem List.rtakeWhile_nil
modified theorem Equiv.Perm.isCycleOn_empty
modified theorem rank_fin_fun
modified theorem xor_comm
modified theorem Real.volume_singleton
modified theorem Filter.isBounded_top
modified theorem Set.left_mem_Ioc
modified theorem Set.left_mem_Ioo
modified theorem Set.right_mem_Ico
modified theorem Set.right_mem_Ioo
modified theorem Cardinal.mk_set