Theorem: Weight.pair'_of_fraction (Weights/Dimension2.lean)

State before:
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ pair' (of_fraction d a b) z = ↑a * z 2 + ↑b * (z 1 + z 2)
Tactic:
simp only [pair', of_fraction, Fin.sum_univ_three, cons_val_zero, cons_val_one, head_cons,
  cons_val_two, tail_cons, Nat.cast_add]
State after:
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ z 0 * ↑0 + z 1 * ↑b + z 2 * (↑a + ↑b) = ↑a * z 2 + ↑b * (z 1 + z 2)

State before:
d a b : ℕ
z : Fin (Nat.succ 2) → ℤ
⊢ z 0 * ↑0 + z 1 * ↑b + z 2 * (↑a + ↑b) = ↑a * z 2 + ↑b * (z 1 + z 2)
Tactic:
ring
State after:
no goals