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

State before:
x y : Nat
⊢ (x + 1).pair y = (x + 1 + y).tri + (x + 1)
Tactic:
rfl
State after:
no goals

State before:
x y : Nat
⊢ (x + 1 + y).tri + (x + 1) = (x + y + 1).tri + (x + 1)
Tactic:
rw [Nat.add_right_comm _ y 1]
State after:
no goals

State before:
x y : Nat
⊢ (x + y + 1).tri + (x + 1) = (x + y).tri + (x + y) + 1 + (x + 1)
Tactic:
rfl
State after:
no goals

State before:
x y : Nat
⊢ (x + y).tri + (x + y) + 1 + (x + 1) = (x + y).tri + x + y + 1 + (x + 1)
Tactic:
rw [Nat.add_assoc _ x y]
State after:
no goals

State before:
x y : Nat
⊢ (x + y).tri + x + y + 1 + (x + 1) = x.pair y + y + 1 + (x + 1)
Tactic:
rfl
State after:
no goals

State before:
x y : Nat
⊢ x.pair y + y + 1 + (x + 1) = x.pair y + y + (x + 1) + 1
Tactic:
rw [Nat.add_right_comm _ (x+1) 1]
State after:
no goals

State before:
x y : Nat
⊢ x.pair y + y + (x + 1) + 1 = x.pair y + y + x + 1 + 1
Tactic:
rw [Nat.add_assoc _ x 1]
State after:
no goals

State before:
x y : Nat
⊢ x.pair y + y + x + 1 + 1 = x.pair y + (y + x) + 1 + 1
Tactic:
rw [Nat.add_assoc _ y x]
State after:
no goals

State before:
x y : Nat
⊢ x.pair y + (y + x) + 1 + 1 = x.pair y + (x + y) + 1 + 1
Tactic:
rw [Nat.add_comm x y]
State after:
no goals