α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ Option.map (fun a' => (a', tail s)) (get? s 0) = none → s = nil
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ destruct s = none → s = nil
dsimp [destruct]
case none
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
⊢ s = nil

case some
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
val✝ : α
f0 : get? s 0 = some val✝
h : Option.map (fun a' => (a', tail s)) (some val✝) = none
⊢ s = nil
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ Option.map (fun a' => (a', tail s)) (get? s 0) = none → s = nil
induction' f0 : get? s 0 <;> intro h
case none.a
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
⊢ ↑s = ↑nil
case none
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
⊢ s = nil
apply Subtype.eq
case none.a.h
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
n : ℕ
⊢ ↑s n = ↑nil n
case none.a
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
⊢ ↑s = ↑nil
funext n
case none.a.h.zero
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
⊢ ↑s Nat.zero = ↑nil Nat.zero

case none.a.h.succ
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
n : ℕ
IH : ↑s n = ↑nil n
⊢ ↑s (Nat.succ n) = ↑nil (Nat.succ n)
case none.a.h
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
n : ℕ
⊢ ↑s n = ↑nil n
induction' n with n IH
no goals
case none.a.h.zero
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
⊢ ↑s Nat.zero = ↑nil Nat.zero

case none.a.h.succ
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
f0 : get? s 0 = none
h : Option.map (fun a' => (a', tail s)) none = none
n : ℕ
IH : ↑s n = ↑nil n
⊢ ↑s (Nat.succ n) = ↑nil (Nat.succ n)
exacts [f0, s.2 IH]
no goals
case some
α : Type u
β : Type v
γ : Type w
s : Seq α
x✝ : Option α
f0✝ : get? s 0 = x✝
val✝ : α
f0 : get? s 0 = some val✝
h : Option.map (fun a' => (a', tail s)) (some val✝) = none
⊢ s = nil
contradiction