Theorem: Nat.div_lt_if_mod (MLIR/Util/KDTensor.lean)

State before:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix / modulus < bound / modulus
Tactic:
rewrite [Nat.div_lt_iff_lt_mul, Nat.mul_cancel_right]
State after:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix < bound

case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus

State before:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ ix < bound

case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Tactic:
apply IX
State after:
case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus

State before:
case MODZERO
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ bound % modulus = 0

ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Tactic:
apply DIV
State after:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus

State before:
ix bound modulus : ℕ
IX : ix < bound
MODULUS : modulus > 0
DIV : bound % modulus = 0
⊢ 0 < modulus
Tactic:
apply MODULUS
State after:
no goals