Init.Data.Int.Pow duplicates

Stream: lean4

[Aaron Liu]

The file Init.Data.Int.Pow has 9 theorems, 4 of which are duplicates.

prelude
import Init.Data.Int.Pow

-- found using loogle and type_of%

#check Nat.pow_le_pow_of_le_left
#check Nat.pow_le_pow_left
#check Int.pow_le_pow_of_le_left

#check Nat.pow_le_pow_of_le_right
#check Nat.pow_le_pow_right
#check Int.pow_le_pow_of_le_right

#check Nat.pos_pow_of_pos
#check Nat.pow_pos
#check Int.pos_pow_of_pos

#check Lean.Omega.Int.ofNat_pow
#check Int.natCast_pow

Should they be removed?

[Eric Wieser]

docs#Int.pos_pow_of_pos looks like it was stated incorrectly

[Eric Wieser]

Same for all the Int lemmas that clash with Nat lemmas

[Ruben Van de Velde]

Lean.Omega. is an implementation detail to the omega tactic

[Ruben Van de Velde]

Possibly one of the Nat ones each should be deprecated

[Ruben Van de Velde]

And the Int ones should be restated to be about Int instead, as Eric points out

[Kim Morrison]

Sorry, these have been on my radar for some time (Markus has a tool that identified them automatically) but haven't got there yet.

[Kim Morrison]

These should all be cleaned up in lean#7113.