Theorem: rot_add_neg_left (Instructor/Lectures/grad/case_study_symmetries_key.lean)

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

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

⊢ -r0 + r0 = 0

case r120

⊢ -r120 + r120 = 0

case r240

⊢ -r240 + r240 = 0

State before:
case r0

⊢ -r0 + r0 = 0

case r120

⊢ -r120 + r120 = 0

case r240

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

State before:
case r240

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