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

State before:
d a b k : ℕ
z : Fin 3 → ℤ
⊢ pair' (of_fraction d (k * a) (k * b)) z = ↑k * pair' (of_fraction d a b) z
Tactic:
simp_rw [pair'_of_fraction, Nat.cast_mul]
State after:
d a b k : ℕ
z : Fin 3 → ℤ
⊢ ↑k * ↑a * z 2 + ↑k * ↑b * (z 1 + z 2) = ↑k * (↑a * z 2 + ↑b * (z 1 + z 2))

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