Theorem: rot_add_vadd (Instructor/Lectures/grad/vector_spaces.lean)

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

State before:
g₁ g₂ : Rotation
p : State
⊢ g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
Tactic:
cases g₁
State after:
case r0
g₂ : Rotation
p : State
⊢ r0 + g₂ +ᵥ p = r0 +ᵥ (g₂ +ᵥ p)

case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)

State before:
case r0
g₂ : Rotation
p : State
⊢ r0 + g₂ +ᵥ p = r0 +ᵥ (g₂ +ᵥ p)

case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)
Tactic:
repeat {
  cases g₂
  repeat {
    cases p
    repeat rfl
  }
}
State after:
case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)

case r240
g₂ : Rotation
p : State
⊢ r240 + g₂ +ᵥ p = r240 +ᵥ (g₂ +ᵥ p)

State before:
case r120
g₂ : Rotation
p : State
⊢ r120 + g₂ +ᵥ p = r120 +ᵥ (g₂ +ᵥ p)
Tactic:
cases g₂
State after:
case r120.r0
p : State
⊢ r120 + r0 +ᵥ p = r120 +ᵥ (r0 +ᵥ p)

case r120.r120
p : State
⊢ r120 + r120 +ᵥ p = r120 +ᵥ (r120 +ᵥ p)

case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)

State before:
case r120.r0
p : State
⊢ r120 + r0 +ᵥ p = r120 +ᵥ (r0 +ᵥ p)

case r120.r120
p : State
⊢ r120 + r120 +ᵥ p = r120 +ᵥ (r120 +ᵥ p)

case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)
Tactic:
repeat {
  cases p
  repeat rfl
}
State after:
case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)

State before:
case r120.r240
p : State
⊢ r120 + r240 +ᵥ p = r120 +ᵥ (r240 +ᵥ p)
Tactic:
cases p
State after:
case r120.r240.heading
h✝ : K
unit✝ : ℕ
⊢ r120 + r240 +ᵥ heading h✝ unit✝ = r120 +ᵥ (r240 +ᵥ heading h✝ unit✝)

State before:
case r120.r120.heading
h✝ : K
unit✝ : ℕ
⊢ r120 + r120 +ᵥ heading h✝ unit✝ = r120 +ᵥ (r120 +ᵥ heading h✝ unit✝)
Tactic:
repeat rfl
State after:
no goals

State before:
case r120.r120.heading
h✝ : K
unit✝ : ℕ
⊢ r120 + r120 +ᵥ heading h✝ unit✝ = r120 +ᵥ (r120 +ᵥ heading h✝ unit✝)
Tactic:
rfl
State after:
no goals