Theorem: pair_add (examples/DoublePendulum2d.lean)

State before:
X : Type u_1
Y : Type u_2
inst✝¹ : Add X
inst✝ : Add Y
x x' : X
y y' : Y
⊢ (x, y) + (x', y') = (x + x', y + y')
Tactic:
simp[HAdd.hAdd, Add.add]
State after:
no goals