Theorem: Nat.snd_pair (GMLInit/Data/Nat/Coding/Prod.lean)

State before:
x y : Nat
⊢ (x.pair y).snd = y
Tactic:
unfold Nat.snd
State after:
x y : Nat
⊢ (x.pair y).split.fst - ↑(x.pair y).split.snd = y

State before:
x y : Nat
⊢ (x.pair y).split.fst - ↑(x.pair y).split.snd = y
Tactic:
rw [Nat.split_pair_snd]
State after:
x y : Nat
⊢ (x.pair y).split.fst - x = y

State before:
x y : Nat
⊢ (x.pair y).split.fst - x = y
Tactic:
rw [Nat.split_pair_fst]
State after:
x y : Nat
⊢ x + y - x = y

State before:
x y : Nat
⊢ x + y - x = y
Tactic:
rw [Nat.add_sub_cancel_left]
State after:
no goals