Theorem: rot_add_vadd (Instructor/Lectures/grad/case_study_symmetries_key.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:
no goals

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

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

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

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

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

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

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

⊢ r240 + r240 +ᵥ s0 = r240 +ᵥ (r240 +ᵥ s0)

case r240.r240.s120

⊢ r240 + r240 +ᵥ s120 = r240 +ᵥ (r240 +ᵥ s120)

case r240.r240.s240

⊢ r240 + r240 +ᵥ s240 = r240 +ᵥ (r240 +ᵥ s240)

State before:
case r240.r240.s0

⊢ r240 + r240 +ᵥ s0 = r240 +ᵥ (r240 +ᵥ s0)

case r240.r240.s120

⊢ r240 + r240 +ᵥ s120 = r240 +ᵥ (r240 +ᵥ s120)

case r240.r240.s240

⊢ r240 + r240 +ᵥ s240 = r240 +ᵥ (r240 +ᵥ s240)
Tactic:
repeat rfl
State after:
no goals

State before:
case r240.r240.s240

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