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

State before:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑(x.succ.pair y) = ↑(x.pair y) + n
Tactic:
simp [pair, Nat.add_mul]
State after:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑x * n + n + ↑y = ↑x * n + ↑y + n

State before:
m n : ℕ
x : Fin m
y : Fin n
⊢ ↑x * n + n + ↑y = ↑x * n + ↑y + n
Tactic:
ring
State after:
no goals