Theorem: rot_zero_add (Instructor/Lectures/grad/vector_spaces.lean)

State before:
⊢ ∀ (a : Rotation), 0 + a = a
Tactic:
intro a
State after:
a : Rotation
⊢ 0 + a = a

State before:
a : Rotation
⊢ 0 + a = a
Tactic:
cases a
State after:
case r0

⊢ 0 + r0 = r0

case r120

⊢ 0 + r120 = r120

case r240

⊢ 0 + r240 = r240

State before:
case r0

⊢ 0 + r0 = r0

case r120

⊢ 0 + r120 = r120

case r240

⊢ 0 + r240 = r240
Tactic:
repeat { rfl }
State after:
no goals

State before:
case r240

⊢ 0 + r240 = r240
Tactic:
rfl
State after:
no goals