Theorem: rot_state_vadd_vsub' (Instructor/Lectures/grad/case_study_symmetries_key.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

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

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

State before:
case r240
p : State
⊢ r240 +ᵥ p -ᵥ p = r240
Tactic:
cases p
State after:
case r240.s0

⊢ r240 +ᵥ s0 -ᵥ s0 = r240

case r240.s120

⊢ r240 +ᵥ s120 -ᵥ s120 = r240

case r240.s240

⊢ r240 +ᵥ s240 -ᵥ s240 = r240

State before:
case r240.s0

⊢ r240 +ᵥ s0 -ᵥ s0 = r240

case r240.s120

⊢ r240 +ᵥ s120 -ᵥ s120 = r240

case r240.s240

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

State before:
case r240.s240

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