α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
⊢ ∃ b, b ∈ t ∧ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h : a ∈ s
⊢ ∃ b, b ∈ t ∧ R a b
let ⟨n, h⟩ := exists_get?_of_mem h
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s n))
⊢ ∃ b, b ∈ t ∧ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
⊢ ∃ b, b ∈ t ∧ R a b
dsimp only [get?, head] at h
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s n))
s' : WSeq α
sd : some (a, s') ∈ destruct (drop s n)
⊢ ∃ b, b ∈ t ∧ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s n))
⊢ ∃ b, b ∈ t ∧ R a b
let ⟨some (_, s'), sd, rfl⟩ := Computation.exists_of_mem_map h
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s n))
s' : WSeq α
sd : some (a, s') ∈ destruct (drop s n)
b : β
t' : WSeq β
td : some (b, t') ∈ destruct (drop t n)
ab : R a b
right✝ : LiftRel R s' t'
⊢ ∃ b, b ∈ t ∧ R a b
α : Type u
β : Type v
γ : Type w
R : α → β → Prop
s : WSeq α
t : WSeq β
H : LiftRel R s t
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s n))
s' : WSeq α
sd : some (a, s') ∈ destruct (drop s n)
⊢ ∃ b, b ∈ t ∧ R a b
let ⟨some (b, t'), td, ⟨ab, _⟩⟩ := (liftRel_dropn_destruct H n).left sd