case nil
ι : Type ?u.349607
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
⊢ reduceOption (map (Option.map f) []) = map f (reduceOption [])

case cons
ι : Type ?u.349607
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
hd : Option α
tl : List (Option α)
hl : reduceOption (map (Option.map f) tl) = map f (reduceOption tl)
⊢ reduceOption (map (Option.map f) (hd :: tl)) = map f (reduceOption (hd :: tl))
ι : Type ?u.349607
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
f : α → β
⊢ reduceOption (map (Option.map f) l) = map f (reduceOption l)
induction' l with hd tl hl
no goals
case nil
ι : Type ?u.349607
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
⊢ reduceOption (map (Option.map f) []) = map f (reduceOption [])
simp only [reduceOption_nil, map_nil]
no goals
case cons
ι : Type ?u.349607
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
f : α → β
hd : Option α
tl : List (Option α)
hl : reduceOption (map (Option.map f) tl) = map f (reduceOption tl)
⊢ reduceOption (map (Option.map f) (hd :: tl)) = map f (reduceOption (hd :: tl))
cases hd <;>
   simpa [true_and_iff, Option.map_some', map, eq_self_iff_true,
     reduceOption_cons_of_some] using hl