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

State before:
n : Nat
⊢ n.fst.pair n.snd = n
Tactic:
unfold pair Nat.fst Nat.snd
State after:
n : Nat
⊢ (↑n.split.snd + (n.split.fst - ↑n.split.snd)).tri + ↑n.split.snd = n

State before:
n : Nat
⊢ (↑n.split.snd + (n.split.fst - ↑n.split.snd)).tri + ↑n.split.snd = n
Tactic:
match h : split n with
| ⟨t,⟨s,hs⟩⟩ =>
  rw [Nat.add_comm s, Nat.sub_add_cancel (Nat.le_of_lt_succ hs)]
  rw [←split_eq n, h]
State after:
no goals

State before:
n t s : Nat
hs : s < t + 1
h : n.split = ⟨t, ⟨s, hs⟩⟩
⊢ (↑⟨t, ⟨s, hs⟩⟩.snd + (⟨t, ⟨s, hs⟩⟩.fst - ↑⟨t, ⟨s, hs⟩⟩.snd)).tri + ↑⟨t, ⟨s, hs⟩⟩.snd = n
Tactic:
rw [Nat.add_comm s, Nat.sub_add_cancel (Nat.le_of_lt_succ hs)]
State after:
n t s : Nat
hs : s < t + 1
h : n.split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + ↑⟨t, ⟨s, hs⟩⟩.snd = n

State before:
n t s : Nat
hs : s < t + 1
h : n.split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + ↑⟨t, ⟨s, hs⟩⟩.snd = n
Tactic:
rw [←split_eq n, h]
State after:
no goals