Theorem: rot_state_vsub_vadd' (Instructor/Lectures/grad/case_study_symmetries_key.lean)

State before:
⊢ ∀ (p1 p2 : State), p1 -ᵥ p2 +ᵥ p2 = p1
Tactic:
intro p1 p2
State after:
p1 p2 : State
⊢ p1 -ᵥ p2 +ᵥ p2 = p1

State before:
p1 p2 : State
⊢ p1 -ᵥ p2 +ᵥ p2 = p1
Tactic:
cases p1
State after:
case s0
p2 : State
⊢ s0 -ᵥ p2 +ᵥ p2 = s0

case s120
p2 : State
⊢ s120 -ᵥ p2 +ᵥ p2 = s120

case s240
p2 : State
⊢ s240 -ᵥ p2 +ᵥ p2 = s240

State before:
case s0
p2 : State
⊢ s0 -ᵥ p2 +ᵥ p2 = s0

case s120
p2 : State
⊢ s120 -ᵥ p2 +ᵥ p2 = s120

case s240
p2 : State
⊢ s240 -ᵥ p2 +ᵥ p2 = s240
Tactic:
repeat { 
  cases p2 
  repeat rfl
}
State after:
no goals

State before:
case s240
p2 : State
⊢ s240 -ᵥ p2 +ᵥ p2 = s240
Tactic:
cases p2
State after:
case s240.s0

⊢ s240 -ᵥ s0 +ᵥ s0 = s240

case s240.s120

⊢ s240 -ᵥ s120 +ᵥ s120 = s240

case s240.s240

⊢ s240 -ᵥ s240 +ᵥ s240 = s240

State before:
case s240.s0

⊢ s240 -ᵥ s0 +ᵥ s0 = s240

case s240.s120

⊢ s240 -ᵥ s120 +ᵥ s120 = s240

case s240.s240

⊢ s240 -ᵥ s240 +ᵥ s240 = s240
Tactic:
repeat rfl
State after:
no goals

State before:
case s240.s240

⊢ s240 -ᵥ s240 +ᵥ s240 = s240
Tactic:
rfl
State after:
no goals