case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : Option (α × WSeq α)
om : o ∈ destruct (drop s n)
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩
case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : Option (α × WSeq α)
om : o ∈ destruct (drop s n)
this : Prod.fst <$> o = some a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : Option (α × WSeq α)
om : o ∈ destruct (drop s n)
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
have := Computation.mem_unique (Computation.mem_map _ om) h
case mk.intro.none
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
om : none ∈ destruct (drop s n)
this : Prod.fst <$> none = some a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)

case mk.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : α × WSeq α
om : some o ∈ destruct (drop s n)
this : Prod.fst <$> some o = some a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
case mk.intro
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : Option (α × WSeq α)
om : o ∈ destruct (drop s n)
this : Prod.fst <$> o = some a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
cases' o with o
case mk.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : α × WSeq α
om : some o ∈ destruct (drop s n)
i : o.fst = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
case mk.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : α × WSeq α
om : some o ∈ destruct (drop s n)
this : Prod.fst <$> some o = some a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
injection this with i
case mk.intro.some.mk
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
a' : α
s' : WSeq α
om : some (a', s') ∈ destruct (drop s n)
i : (a', s').fst = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
case mk.intro.some
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
o : α × WSeq α
om : some o ∈ destruct (drop s n)
i : o.fst = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
cases' o with a' s'
case mk.intro.some.mk
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
a' : α
s' : WSeq α
om : some (a', s') ∈ destruct (drop s n)
i : a' = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
case mk.intro.some.mk
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
a' : α
s' : WSeq α
om : some (a', s') ∈ destruct (drop s n)
i : (a', s').fst = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
dsimp at i
case mk.intro.some.mk
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
a' : α
s' : WSeq α
om : some (a, s') ∈ destruct (drop s n)
i : a' = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
case mk.intro.some.mk
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
a' : α
s' : WSeq α
om : some (a', s') ∈ destruct (drop s n)
i : a' = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
rw [i] at om
no goals
case mk.intro.some.mk
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
a' : α
s' : WSeq α
om : some (a, s') ∈ destruct (drop s n)
i : a' = a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
exact ⟨_, om⟩
no goals
case mk.intro.none
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
h✝ : a ∈ s
n : ℕ
h : some a ∈ get? s n
om : none ∈ destruct (drop s n)
this : Prod.fst <$> none = some a
⊢ ∃ s', some (a, s') ∈ destruct (drop s n)
injection this