case nil
ι : Type ?u.368529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ x : Option α
⊢ reduceOption (concat [] x) = reduceOption [] ++ Option.toList x

case cons
ι : Type ?u.368529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ hd : Option α
tl : List (Option α)
hl : ∀ (x : Option α), reduceOption (concat tl x) = reduceOption tl ++ Option.toList x
x : Option α
⊢ reduceOption (concat (hd :: tl) x) = reduceOption (hd :: tl) ++ Option.toList x
ι : Type ?u.368529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
x : Option α
⊢ reduceOption (concat l x) = reduceOption l ++ Option.toList x
induction' l with hd tl hl generalizing x
no goals
case nil
ι : Type ?u.368529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ x : Option α
⊢ reduceOption (concat [] x) = reduceOption [] ++ Option.toList x
cases x <;> simp [Option.toList]
case cons
ι : Type ?u.368529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), reduceOption tl ++ reduceOption [x] = reduceOption tl ++ Option.toList x
⊢ reduceOption (concat (hd :: tl) x) = reduceOption (hd :: tl) ++ Option.toList x
case cons
ι : Type ?u.368529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ hd : Option α
tl : List (Option α)
hl : ∀ (x : Option α), reduceOption (concat tl x) = reduceOption tl ++ Option.toList x
x : Option α
⊢ reduceOption (concat (hd :: tl) x) = reduceOption (hd :: tl) ++ Option.toList x
simp only [concat_eq_append, reduceOption_append] at hl
no goals
case cons
ι : Type ?u.368529
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x✝ hd : Option α
tl : List (Option α)
x : Option α
hl : ∀ (x : Option α), reduceOption tl ++ reduceOption [x] = reduceOption tl ++ Option.toList x
⊢ reduceOption (concat (hd :: tl) x) = reduceOption (hd :: tl) ++ Option.toList x
cases hd <;> simp [hl, reduceOption_append]