Theorem: Option.first_append (GMLInit/Data/Option.lean)

State before:
α : Type u_1
xs ys : List (Option α)
⊢ first (xs ++ ys) = HOrElse.hOrElse (first xs) fun x => first ys
Tactic:
induction xs with
| nil => rfl
| cons x xs ih => simp [orElse_assoc, ih]
State after:
no goals

State before:
case nil
α : Type u_1
ys : List (Option α)
⊢ first ([] ++ ys) = HOrElse.hOrElse (first []) fun x => first ys
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
ys : List (Option α)
x : Option α
xs : List (Option α)
ih : first (xs ++ ys) = HOrElse.hOrElse (first xs) fun x => first ys
⊢ first (x :: xs ++ ys) = HOrElse.hOrElse (first (x :: xs)) fun x => first ys
Tactic:
simp [orElse_assoc, ih]
State after:
no goals