Theorem: Point.add_y (LeanCourse/Lectures/Lecture8Before.lean)

State before:
n : ℕ
a b : Point
⊢ (a + b).y = a.y + b.y
Tactic:
rfl
State after:
no goals