Theorem: rot_state_vadd_vsub' (Instructor/Lectures/grad/vector_spaces.lean)

State before:
⊢ ∀ (g : Rotation) (p : State), g +ᵥ p -ᵥ p = g
Tactic:
intros g p
State after:
g : Rotation
p : State
⊢ g +ᵥ p -ᵥ p = g

State before:
g : Rotation
p : State
⊢ g +ᵥ p -ᵥ p = g
Tactic:
cases g
State after:
case r0
p : State
⊢ r0 +ᵥ p -ᵥ p = r0

case r120
p : State
⊢ r120 +ᵥ p -ᵥ p = r120

case r240
p : State
⊢ r240 +ᵥ p -ᵥ p = r240

State before:
case r0
p : State
⊢ r0 +ᵥ p -ᵥ p = r0
Tactic:
cases p
State after:
case r0.heading
h✝ : K
unit✝ : ℕ
⊢ r0 +ᵥ heading h✝ unit✝ -ᵥ heading h✝ unit✝ = r0