case mk
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
⊢ a ∈ think { val := f, property := al } ↔ a ∈ { val := f, property := al }
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
⊢ a ∈ think s ↔ a ∈ s
cases' s with f al
case mk
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f
case mk
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
⊢ a ∈ think { val := f, property := al } ↔ a ∈ { val := f, property := al }
change (some (some a) ∈ some none::f) ↔ some (some a) ∈ f
case mk.mp
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f

case mk.mpr
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f
case mk
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f
constructor <;> intro h
case mk.mp
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ some none :: f
⊢ ¬some (some a) = some none
case mk.mp
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f
apply (Stream'.eq_or_mem_of_mem_cons h).resolve_left
case mk.mp
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ some none :: f
a✝ : some (some a) = some none
⊢ False
case mk.mp
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ some none :: f
⊢ ¬some (some a) = some none
intro
no goals
case mk.mp
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ some none :: f
a✝ : some (some a) = some none
⊢ False
injections
no goals
case mk.mpr
α : Type u
β : Type v
γ : Type w
a : α
f : Stream' (Option (Option α))
al : IsSeq f
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f
apply Stream'.mem_cons_of_mem _ h