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

State before:
n m : ℕ
⊢ ∀ (i : ℕ), transpose_remap m n (transpose_remap n m i) = i
Tactic:
simp [transpose_remap, Function.comp]
State after:
n m : ℕ
⊢ ∀ (i : ℕ), n * ((m * (i % n) + i / n) % m) + (m * (i % n) + i / n) / m = i

State before:
n m : ℕ
⊢ ∀ (i : ℕ), n * ((m * (i % n) + i / n) % m) + (m * (i % n) + i / n) / m = i
Tactic:
intro i
State after:
n m i : ℕ
⊢ n * ((m * (i % n) + i / n) % m) + (m * (i % n) + i / n) / m = i

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