Theorem: rot_state_vsub_vadd' (Instructor/Lectures/grad/vector_spaces.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 heading
p2 : State
h✝ : K
unit✝ : ℕ
⊢ heading h✝ unit✝ -ᵥ p2 +ᵥ p2 = heading h✝ unit✝

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