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

State before:
d a₁ b₁ a₂ b₂ : ℕ
⊢ pair' (of_fraction d (a₁ + a₂) (b₁ + b₂)) = pair' (of_fraction d a₁ b₁) + pair' (of_fraction d a₂ b₂)
Tactic:
ext z
State after:
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

State before:
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
Tactic:
simp_rw [Pi.add_apply, pair'_of_fraction, Nat.cast_add]
State after:
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))

State before:
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))
Tactic:
ring
State after:
no goals