CompLemmas

Stream: mathlib4

[Scott Morrison]

Mathlib.Init.Data.Int.CompLemmas was ported from core, and was never really intended for outside use. Nevertheless, people started using it. (Surprise!)

#7142 removes one out of the two uses in Mathlib.

If anyone would like to do the other in a separate PR, please do! You would need to reprove

theorem Int.natAbs_add_nonneg {a b : ℤ} (wa : 0 ≤ a) (wb : 0 ≤ b) :
    Int.natAbs (a + b) = Int.natAbs a + Int.natAbs b := sorry

theorem Int.natAbs_add_neg {a b : ℤ} (wa : a < 0) (wb : b < 0) :
    Int.natAbs (a + b) = Int.natAbs a + Int.natAbs b := sorry

I think after that we should just delete the file.

[Mario Carneiro]

I want that in std

[Mario Carneiro]

the latter theorem is true as long as the variables are nonpositive

[Kevin Buzzard]

My guess is that people start using it because exact? finds random stuff? I used to see this with library_search in Lean 3, random lemmas being used by my students that had norm_num in the name or really weird names, which were just internal things used by norm_num but library_search found them because they happened to be exactly what someone wanted.

[Ruben Van de Velde]

I think these were simp lemmas that were in the prelude in lean3, or was that another file?