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

State before:
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ ⟨t, ⟨s, hs⟩⟩.fst = x + y
Tactic:
apply Nat.tri_add_inj (Nat.le_of_lt_succ hs) (Nat.le_add_right x y)
State after:
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x + y).tri + x

State before:
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x + y).tri + x
Tactic:
transitivity (tri (split (pair x y)).fst + (split (pair x y)).snd)
State after:
case left
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x.pair y).split.fst.tri + ↑(x.pair y).split.snd

case right
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x + y).tri + x

State before:
case left
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ t.tri + s = (x.pair y).split.fst.tri + ↑(x.pair y).split.snd
Tactic:
rw [h]
State after:
no goals

State before:
case right
x y t s : Nat
hs : s < t + 1
h : (x.pair y).split = ⟨t, ⟨s, hs⟩⟩
⊢ (x.pair y).split.fst.tri + ↑(x.pair y).split.snd = (x + y).tri + x
Tactic:
rw [split_eq, pair]
State after:
no goals