simp_rw [Pi.add_apply, pair'_of_fraction, Nat.cast_add]
case h
d a₁ b₁ a₂ b₂ : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ pair' (of_fraction d (a₁ + a₂) (b₁ + b₂)) z = (pair' (of_fraction d a₁ b₁) + pair' (of_fraction d a₂ b₂)) z
case h
d a₁ b₁ a₂ b₂ : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ (↑a₁ + ↑a₂) * z 2 + (↑b₁ + ↑b₂) * (z 1 + z 2) = ↑a₁ * z 2 + ↑b₁ * (z 1 + z 2) + (↑a₂ * z 2 + ↑b₂ * (z 1 + z 2))