Theorem: transpose_remap_bound (MLIR/Dialects/ToyModel.lean)

State before:
n m : ℕ
⊢ ∀ (i : ℕ), i < n * m → transpose_remap n m i < n * m
Tactic:
intro i h
State after:
n m i : ℕ
h : i < n * m
⊢ transpose_remap n m i < n * m

State before:
n m i : ℕ
h : i < n * m
⊢ transpose_remap n m i < n * m
Tactic:
simp [transpose_remap]
State after:
n m i : ℕ
h : i < n * m
⊢ m * (i % n) + i / n < n * m

State before:
n m i : ℕ
h : i < n * m
⊢ m * (i % n) + i / n < n * m
Tactic:
sorry
State after:
no goals