Theorem: bool_or_assoc (Katydid/Std/AlgebraExamples.lean)

State before:
⊢ ∀ (a b c : Bool), (a || b || c) = (a || (b || c))
Tactic:
intro a b c
State after:
a b c : Bool
⊢ (a || b || c) = (a || (b || c))

State before:
a b c : Bool
⊢ (a || b || c) = (a || (b || c))
Tactic:
cases a with
| false =>
  simp
| true =>
  simp
State after:
no goals

State before:
case false
b c : Bool
⊢ (false || b || c) = (false || (b || c))
Tactic:
simp
State after:
no goals

State before:
case true
b c : Bool
⊢ (true || b || c) = (true || (b || c))
Tactic:
simp
State after:
no goals