case nil
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ length (reduceOption []) = length [] ↔ ∀ (x : Option α), x ∈ [] → Option.isSome x = true

case cons
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
hd : Option α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
⊢ length (reduceOption (hd :: tl)) = length (hd :: tl) ↔ ∀ (x : Option α), x ∈ hd :: tl → Option.isSome x = true
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
⊢ length (reduceOption l) = length l ↔ ∀ (x : Option α), x ∈ l → Option.isSome x = true
induction' l with hd tl hl
no goals
case nil
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
⊢ length (reduceOption []) = length [] ↔ ∀ (x : Option α), x ∈ [] → Option.isSome x = true
simp only [forall_const, reduceOption_nil, not_mem_nil, forall_prop_of_false, eq_self_iff_true,
  length, not_false_iff]
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
⊢ length (reduceOption (none :: tl)) = length (none :: tl) ↔ ∀ (x : Option α), x ∈ none :: tl → Option.isSome x = true

case cons.some
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
val✝ : α
⊢ length (reduceOption (some val✝ :: tl)) = length (some val✝ :: tl) ↔
    ∀ (x : Option α), x ∈ some val✝ :: tl → Option.isSome x = true
case cons
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
hd : Option α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
⊢ length (reduceOption (hd :: tl)) = length (hd :: tl) ↔ ∀ (x : Option α), x ∈ hd :: tl → Option.isSome x = true
cases hd
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
⊢ ¬length (reduceOption tl) = length tl + 1
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
⊢ length (reduceOption (none :: tl)) = length (none :: tl) ↔ ∀ (x : Option α), x ∈ none :: tl → Option.isSome x = true
simp only [mem_cons, forall_eq_or_imp, Bool.coe_sort_false, false_and_iff,
  reduceOption_cons_of_none, length, Option.isSome_none, iff_false_iff]
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
H : length (reduceOption tl) = length tl + 1
⊢ False
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
⊢ ¬length (reduceOption tl) = length tl + 1
intro H
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
H : length (reduceOption tl) = length tl + 1
this : length (reduceOption tl) ≤ length tl
⊢ False
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
H : length (reduceOption tl) = length tl + 1
⊢ False
have := reduceOption_length_le tl
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
H : length (reduceOption tl) = length tl + 1
this : length tl + 1 ≤ length tl
⊢ False
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
H : length (reduceOption tl) = length tl + 1
this : length (reduceOption tl) ≤ length tl
⊢ False
rw [H] at this
no goals
case cons.none
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
H : length (reduceOption tl) = length tl + 1
this : length tl + 1 ≤ length tl
⊢ False
exact absurd (Nat.lt_succ_self _) (not_lt_of_le this)
no goals
case cons.some
ι : Type ?u.351472
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
tl : List (Option α)
hl : length (reduceOption tl) = length tl ↔ ∀ (x : Option α), x ∈ tl → Option.isSome x = true
val✝ : α
⊢ length (reduceOption (some val✝ :: tl)) = length (some val✝ :: tl) ↔
    ∀ (x : Option α), x ∈ some val✝ :: tl → Option.isSome x = true
simp only [length, add_left_inj, find?, mem_cons, forall_eq_or_imp, Option.isSome_some,
  ← hl, reduceOption, true_and]