Commit 2025-09-10 12:37 d386f9fe

chore: remove triangleRemovalBound positivity extension (#29496) This extension just applies src#SimpleGraph.triangleRemovalBound_pos, discharging an ε ≤ 1 by hoping it is there as a hypothesis(!!), and discharging the other argument by a recursive call to positivity. This is used in a single proof, as

  · have : ε / 9 ≤ 1 := by linarith
    positivity

My complaint here is that this is completely unreadable. One can only understand why the have statement is introduced here by reading meta code. (First of all one has to use show_term or similar to even work out which lemma is being applied, then some grepping to find the positivity extension, and finally the surprising discovery that the have statement is there because the extension goes out look for exactly this fact.)