case nil
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ length (reduceOption []) ≤ length []

case cons
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
hd : Option α
tl : List (Option α)
hl : length (reduceOption tl) ≤ length tl
⊢ length (reduceOption (hd :: tl)) ≤ length (hd :: tl)
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
⊢ length (reduceOption l) ≤ length l
induction' l with hd tl hl
no goals
case nil
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ length (reduceOption []) ≤ length []
simp only [reduceOption_nil, length]
case cons.none
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) ≤ length tl
⊢ length (reduceOption (none :: tl)) ≤ length (none :: tl)

case cons.some
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) ≤ length tl
val✝ : α
⊢ length (reduceOption (some val✝ :: tl)) ≤ length (some val✝ :: tl)
case cons
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
hd : Option α
tl : List (Option α)
hl : length (reduceOption tl) ≤ length tl
⊢ length (reduceOption (hd :: tl)) ≤ length (hd :: tl)
cases hd
no goals
case cons.none
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) ≤ length tl
⊢ length (reduceOption (none :: tl)) ≤ length (none :: tl)
exact Nat.le_succ_of_le hl
no goals
case cons.some
ι : Type ?u.350604
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) ≤ length tl
val✝ : α
⊢ length (reduceOption (some val✝ :: tl)) ≤ length (some val✝ :: tl)
simpa only [length, add_le_add_iff_right, reduceOption_cons_of_some] using hl