α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
α : Type u
β : Type v
γ : Type w
s : WSeq α
a : α
n : ℕ
⊢ some a ∈ get? s n → a ∈ s
revert s
case zero
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ get? s Nat.zero
⊢ a ∈ s

case succ
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
s : WSeq α
h : some a ∈ get? s (Nat.succ n)
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
⊢ ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
induction' n with n IH <;> intro s h
case zero
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
⊢ a ∈ s
case zero
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ get? s Nat.zero
⊢ a ∈ s
dsimp only [get?, head] at h
case zero.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
o : Option (α × WSeq α)
h1 : o ∈ destruct (drop s Nat.zero)
h2 : Prod.fst <$> o = some a
⊢ a ∈ s
case zero
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
⊢ a ∈ s
rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
case zero.intro.intro.none
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
h1 : none ∈ destruct (drop s Nat.zero)
h2 : Prod.fst <$> none = some a
⊢ a ∈ s

case zero.intro.intro.some
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
o : α × WSeq α
h1 : some o ∈ destruct (drop s Nat.zero)
h2 : Prod.fst <$> some o = some a
⊢ a ∈ s
case zero.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
o : Option (α × WSeq α)
h1 : o ∈ destruct (drop s Nat.zero)
h2 : Prod.fst <$> o = some a
⊢ a ∈ s
cases' o with o
case zero.intro.intro.some
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
o : α × WSeq α
h1 : some o ∈ destruct (drop s Nat.zero)
h' : o.fst = a
⊢ a ∈ s
case zero.intro.intro.some
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
o : α × WSeq α
h1 : some o ∈ destruct (drop s Nat.zero)
h2 : Prod.fst <$> some o = some a
⊢ a ∈ s
injection h2 with h'
case zero.intro.intro.some.mk
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
a' : α
s' : WSeq α
h1 : some (a', s') ∈ destruct (drop s Nat.zero)
h' : (a', s').fst = a
⊢ a ∈ s
case zero.intro.intro.some
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
o : α × WSeq α
h1 : some o ∈ destruct (drop s Nat.zero)
h' : o.fst = a
⊢ a ∈ s
cases' o with a' s'
no goals
case zero.intro.intro.some.mk
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
a' : α
s' : WSeq α
h1 : some (a', s') ∈ destruct (drop s Nat.zero)
h' : (a', s').fst = a
⊢ a ∈ s
exact (eq_or_mem_iff_mem h1).2 (Or.inl h'.symm)
no goals
case zero.intro.intro.none
α : Type u
β : Type v
γ : Type w
a : α
s : WSeq α
h : some a ∈ Computation.map (fun x => Prod.fst <$> x) (destruct (drop s Nat.zero))
h1 : none ∈ destruct (drop s Nat.zero)
h2 : Prod.fst <$> none = some a
⊢ a ∈ s
injection h2
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
s : WSeq α
h : some a ∈ get? s (Nat.succ n)
this : some a ∈ get? (tail s) n → a ∈ tail s
⊢ a ∈ s
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
s : WSeq α
h : some a ∈ get? s (Nat.succ n)
⊢ a ∈ s
have := @IH (tail s)
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
s : WSeq α
h : some a ∈ get? s (Nat.succ n)
this : some a ∈ get? s (n + 1) → a ∈ tail s
⊢ a ∈ s
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
s : WSeq α
h : some a ∈ get? s (Nat.succ n)
this : some a ∈ get? (tail s) n → a ∈ tail s
⊢ a ∈ s
rw [get?_tail] at this
no goals
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ get? s n → a ∈ s
s : WSeq α
h : some a ∈ get? s (Nat.succ n)
this : some a ∈ get? s (n + 1) → a ∈ tail s
⊢ a ∈ s
exact mem_of_mem_tail (this h)