-- Mathlib/Data/Seq/Computation.lean
theorem destruct_eq_think {s : Computation α} {s'} : destruct s = Sum.inr s' → s = think s'

Proof state:
α : Type u
s s' : Computation α
⊢ (match ↑s 0 with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think

Tactic:
induction' f0 : s.1 0 with a' <;> intro h

Result:
case none
α : Type u
s s' : Computation α
f0 : ↑s 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

case some
α : Type u
s s' : Computation α
a' : α
f0 : ↑s 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Proof state:
case none.mk
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = (tail ⟨f, al⟩).think

Tactic:
apply Subtype.eq

Result:
case none.mk.a
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ ↑⟨f, al⟩ = ↑(tail ⟨f, al⟩).think

Proof state:
case none
α : Type u
s s' : Computation α
f0 : ↑s 0 = none
h :
  (match none with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
injection h with h'

Result:
case none
α : Type u
s s' : Computation α
f0 : ↑s 0 = none
h' : s.tail = s'
⊢ s = s'.think

Proof state:
case none
α : Type u
s s' : Computation α
f0 : ↑s 0 = none
h' : s.tail = s'
⊢ s = s'.think

Tactic:
rw [← h']

Result:
case none
α : Type u
s s' : Computation α
f0 : ↑s 0 = none
h' : s.tail = s'
⊢ s = s.tail.think

Proof state:
case none.mk.a
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ ↑⟨f, al⟩ = ↑(tail ⟨f, al⟩).think

Tactic:
dsimp [think, tail]

Result:
case none.mk.a
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ f = Stream'.cons none f.tail

Proof state:
α : Type u
s s' : Computation α
⊢ s.destruct = Sum.inr s' → s = s'.think

Tactic:
dsimp [destruct]

Result:
α : Type u
s s' : Computation α
⊢ (match ↑s 0 with
      | none => Sum.inr s.tail
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = s'.think

Proof state:
case none.mk.a
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ f = Stream'.cons none f.tail

Tactic:
rw [← f0]

Result:
case none.mk.a
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ f = Stream'.cons (↑⟨f, al⟩ 0) f.tail

Proof state:
case none
α : Type u
s s' : Computation α
f0 : ↑s 0 = none
h' : s.tail = s'
⊢ s = s.tail.think

Tactic:
obtain ⟨f, al⟩ := s

Result:
case none.mk
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ ⟨f, al⟩ = (tail ⟨f, al⟩).think

Proof state:
case none.mk.a
α : Type u
s' : Computation α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0 : ↑⟨f, al⟩ 0 = none
h' : tail ⟨f, al⟩ = s'
⊢ f = Stream'.cons (↑⟨f, al⟩ 0) f.tail

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

Result:
no goals

Proof state:
case some
α : Type u
s s' : Computation α
a' : α
f0 : ↑s 0 = some a'
h :
  (match some a' with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = s'.think

Tactic:
contradiction

Result:
no goals