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

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

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

⊢ r0 + 0 = r0

case r120

⊢ r120 + 0 = r120

case r240

⊢ r240 + 0 = r240

State before:
case r0

⊢ r0 + 0 = r0

case r120

⊢ r120 + 0 = r120

case r240

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

State before:
case r240

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