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

State before:
⊢ ∀ (a b c : Rotation), a + b + c = a + (b + c)
Tactic:
intros a b c
State after:
a b c : Rotation
⊢ a + b + c = a + (b + c)

State before:
a b c : Rotation
⊢ a + b + c = a + (b + c)
Tactic:
cases a
State after:
case r0
b c : Rotation
⊢ r0 + b + c = r0 + (b + c)

case r120
b c : Rotation
⊢ r120 + b + c = r120 + (b + c)

case r240
b c : Rotation
⊢ r240 + b + c = r240 + (b + c)

State before:
case r0
b c : Rotation
⊢ r0 + b + c = r0 + (b + c)

case r120
b c : Rotation
⊢ r120 + b + c = r120 + (b + c)

case r240
b c : Rotation
⊢ r240 + b + c = r240 + (b + c)
Tactic:
repeat {
  cases b
  repeat {
   cases c
   repeat { rfl }
  }
}
State after:
no goals

State before:
case r240
b c : Rotation
⊢ r240 + b + c = r240 + (b + c)
Tactic:
cases b
State after:
case r240.r0
c : Rotation
⊢ r240 + r0 + c = r240 + (r0 + c)

case r240.r120
c : Rotation
⊢ r240 + r120 + c = r240 + (r120 + c)

case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)

State before:
case r240.r0
c : Rotation
⊢ r240 + r0 + c = r240 + (r0 + c)

case r240.r120
c : Rotation
⊢ r240 + r120 + c = r240 + (r120 + c)

case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)
Tactic:
repeat {
 cases c
 repeat { rfl }
}
State after:
no goals

State before:
case r240.r240
c : Rotation
⊢ r240 + r240 + c = r240 + (r240 + c)
Tactic:
cases c
State after:
case r240.r240.r0

⊢ r240 + r240 + r0 = r240 + (r240 + r0)

case r240.r240.r120

⊢ r240 + r240 + r120 = r240 + (r240 + r120)

case r240.r240.r240

⊢ r240 + r240 + r240 = r240 + (r240 + r240)

State before:
case r240.r240.r0

⊢ r240 + r240 + r0 = r240 + (r240 + r0)

case r240.r240.r120

⊢ r240 + r240 + r120 = r240 + (r240 + r120)

case r240.r240.r240

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

State before:
case r240.r240.r240

⊢ r240 + r240 + r240 = r240 + (r240 + r240)
Tactic:
rfl
State after:
no goals