Theorem: Fin.pair_left_right (LeanColls/MathlibUpstream.lean)

State before:
m n : ℕ
p : Fin (m * n)
⊢ p.pair_left.pair p.pair_right = p
Tactic:
rcases p with ⟨p,hp⟩
State after:
case mk
m n p : ℕ
hp : p < m * n
⊢ ⟨p, hp⟩.pair_left.pair ⟨p, hp⟩.pair_right = ⟨p, hp⟩

State before:
case mk
m n p : ℕ
hp : p < m * n
⊢ ⟨p, hp⟩.pair_left.pair ⟨p, hp⟩.pair_right = ⟨p, hp⟩
Tactic:
simp [pair, pair_left, pair_right]
State after:
case mk
m n p : ℕ
hp : p < m * n
⊢ p / n * n + p % n = p

State before:
case mk
m n p : ℕ
hp : p < m * n
⊢ p / n * n + p % n = p
Tactic:
exact Nat.div_add_mod' p n
State after:
no goals