-- Mathlib/Data/Seq/Seq.lean
theorem destruct_eq_cons {s : Seq α} {a s'} : destruct s = some (a, s') → s = cons a s'

Proof state:
case some.mk
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = cons a (tail ⟨f, al⟩)

Tactic:
apply Subtype.eq

Result:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ↑⟨f, al⟩ = ↑(cons a (tail ⟨f, al⟩))

Proof state:
α : Type u
s : Seq α
a : α
s' : Seq α
⊢ Option.map (fun a' => (a', s.tail)) (s.get? 0) = some (a, s') → s = cons a s'

Tactic:
induction' f0 : get? s 0 with a' <;> intro h

Result:
case none
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = some (a, s')
⊢ s = cons a s'

case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : Option.map (fun a' => (a', s.tail)) (some a') = some (a, s')
⊢ s = cons a s'

Proof state:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = some a :: f.tail

Tactic:
rw [← f0]

Result:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = get? ⟨f, al⟩ 0 :: f.tail

Proof state:
case some
α : Type u
s : Seq α
a : α
s' : Seq α
a' : α
f0 : s.get? 0 = some a'
h : Option.map (fun a' => (a', s.tail)) (some a') = some (a, s')
⊢ s = cons a s'

Tactic:
obtain ⟨f, al⟩ := s

Result:
case some.mk
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h : Option.map (fun a' => (a', tail ⟨f, al⟩)) (some a') = some (a, s')
⊢ ⟨f, al⟩ = cons a s'

Proof state:
case none
α : Type u
s : Seq α
a : α
s' : Seq α
f0 : s.get? 0 = none
h : Option.map (fun a' => (a', s.tail)) none = some (a, s')
⊢ s = cons a s'

Tactic:
contradiction

Result:
no goals

Proof state:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = get? ⟨f, al⟩ 0 :: f.tail

Tactic:
exact (Stream'.eta f).symm

Result:
no goals

Proof state:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ↑⟨f, al⟩ = ↑(cons a (tail ⟨f, al⟩))

Tactic:
dsimp [tail, cons]

Result:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = some a :: f.tail

Proof state:
α : Type u
s : Seq α
a : α
s' : Seq α
⊢ s.destruct = some (a, s') → s = cons a s'

Tactic:
dsimp [destruct]

Result:
α : Type u
s : Seq α
a : α
s' : Seq α
⊢ Option.map (fun a' => (a', s.tail)) (s.get? 0) = some (a, s') → s = cons a s'

Proof state:
case some.mk
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = cons a s'

Tactic:
rw [← h2]

Result:
case some.mk
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = cons a (tail ⟨f, al⟩)

Proof state:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = some a :: f.tail

Tactic:
rw [h1] at f0

Result:
case some.mk.a
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ f = some a :: f.tail

Proof state:
case some.mk
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h : Option.map (fun a' => (a', tail ⟨f, al⟩)) (some a') = some (a, s')
⊢ ⟨f, al⟩ = cons a s'

Tactic:
injections _ h1 h2

Result:
case some.mk
α : Type u
a : α
s' : Seq α
a' : α
f : Stream' (Option α)
al : f.IsSeq
f0 : get? ⟨f, al⟩ 0 = some a'
h1 : a' = a
h2 : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = cons a s'