ι : Type ?u.354270
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → Option.isSome x = true) ↔ none ∈ l
ι : Type ?u.354270
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
⊢ length (reduceOption l) < length l ↔ none ∈ l
rw [(reduceOption_length_le l).lt_iff_ne, Ne, reduceOption_length_eq_iff]
case cons
ι : Type ?u.354270
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → Option.isSome x = true) ↔ none ∈ tail✝
⊢ (Option.isSome head✝ = true → ∃ x, x ∈ tail✝ ∧ Option.isNone x = true) ↔ none = head✝ ∨ none ∈ tail✝
ι : Type ?u.354270
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → Option.isSome x = true) ↔ none ∈ l
induction l <;> simp [*]
case cons
ι : Type ?u.354270
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → Option.isSome x = true) ↔ none ∈ tail✝
⊢ (¬Option.isSome head✝ = true ∨ ∃ x, x ∈ tail✝ ∧ Option.isNone x = true) ↔ ¬Option.isSome head✝ = true ∨ none ∈ tail✝
case cons
ι : Type ?u.354270
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → Option.isSome x = true) ↔ none ∈ tail✝
⊢ (Option.isSome head✝ = true → ∃ x, x ∈ tail✝ ∧ Option.isNone x = true) ↔ none = head✝ ∨ none ∈ tail✝
rw [@eq_comm _ none, ← Option.not_isSome_iff_eq_none, Decidable.imp_iff_not_or]
no goals
case cons
ι : Type ?u.354270
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → Option.isSome x = true) ↔ none ∈ tail✝
⊢ (¬Option.isSome head✝ = true ∨ ∃ x, x ∈ tail✝ ∧ Option.isNone x = true) ↔ ¬Option.isSome head✝ = true ∨ none ∈ tail✝
simp [Option.isNone_iff_eq_none]