no goals
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
h : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b
match s with
| ⟨g, al⟩ =>
let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
cases' o with a
. injection oe
. injection oe with h' ; exact ⟨a, om, h'⟩
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
o : Option α
om : o ∈ g
oe : Option.map f o = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
case none
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
om : none ∈ g
oe : Option.map f none = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b

case some
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
o : Option α
om : o ∈ g
oe : Option.map f o = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
cases' o with a
case some
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
case none
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
om : none ∈ g
oe : Option.map f none = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b

case some
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
. injection oe
no goals
case some
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
. injection oe with h' ; exact ⟨a, om, h'⟩
no goals
case none
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
om : none ∈ g
oe : Option.map f none = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
injection oe
case some
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
case some
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
injection oe with h'
no goals
case some
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : IsSeq g
h : b ∈ map f { val := g, property := al }
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a, a ∈ { val := g, property := al } ∧ f a = b
exact ⟨a, om, h'⟩