-- Mathlib/Data/Seq/Computation.lean
theorem destruct_eq_pure {s : Computation α} {a : α} : destruct s = Sum.inl a → s = pure a

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

Tactic:
induction' n with n IH

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

case some.a.h.succ
α : Type u
s : Computation α
a val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
IH : ↑s n = ↑(pure a) n
⊢ ↑s (n + 1) = ↑(pure a) (n + 1)

Proof state:
case some.a.h.succ
α : Type u
s : Computation α
a val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr s.tail
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
IH : ↑s n = ↑(pure a) n
⊢ ↑s (n + 1) = ↑(pure a) (n + 1)

Tactic:
exact s.2 IH

Result:
no goals

Proof state:
α : Type u
s : Computation α
a : α
⊢ s.destruct = Sum.inl a → s = pure a

Tactic:
dsimp [destruct]

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

Proof state:
case some.a.h.zero
α : Type u
s : Computation α
a val✝ : α
f0 : ↑s 0 = some val✝
h' : val✝ = a
⊢ ↑s 0 = ↑(pure a) 0

Tactic:
rwa [h'] at f0

Result:
no goals

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

Tactic:
contradiction

Result:
no goals

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

Tactic:
apply Subtype.eq

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

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

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

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

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

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

Tactic:
injection h with h'

Result:
case some.a.h.zero
α : Type u
s : Computation α
a val✝ : α
f0 : ↑s 0 = some val✝
h' : val✝ = a
⊢ ↑s 0 = ↑(pure a) 0

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

Tactic:
funext n

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