α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
⊢ (match ↑s 0 with
      | none => Sum.inr (tail s)
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
⊢ destruct s = Sum.inl a → s = pure a
dsimp [destruct]
case none
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
f0 : ↑s 0 = none
h :
  (match none with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a

case some
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
⊢ (match ↑s 0 with
      | none => Sum.inr (tail s)
      | some a => Sum.inl a) =
      Sum.inl a →
    s = pure a
induction' f0 : s.1 0 with _ <;> intro h
no goals
case none
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
f0 : ↑s 0 = none
h :
  (match none with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
contradiction
case some.a
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ ↑s = ↑(pure a)
case some
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ s = pure a
apply Subtype.eq
case some.a.h
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
⊢ ↑s n = ↑(pure a) n
case some.a
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ ↑s = ↑(pure a)
funext n
case some.a.h.zero
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ ↑s Nat.zero = ↑(pure a) Nat.zero

case some.a.h.succ
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
IH : ↑s n = ↑(pure a) n
⊢ ↑s (Nat.succ n) = ↑(pure a) (Nat.succ n)
case some.a.h
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
⊢ ↑s n = ↑(pure a) n
induction' n with n IH
case some.a.h.zero
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h' : val✝ = a
⊢ ↑s Nat.zero = ↑(pure a) Nat.zero
case some.a.h.zero
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
⊢ ↑s Nat.zero = ↑(pure a) Nat.zero
injection h with h'
no goals
case some.a.h.zero
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h' : val✝ = a
⊢ ↑s Nat.zero = ↑(pure a) Nat.zero
rwa [h'] at f0
no goals
case some.a.h.succ
α : Type u
β : Type v
γ : Type w
s : Computation α
a : α
x✝ : Option α
f0✝ : ↑s 0 = x✝
val✝ : α
f0 : ↑s 0 = some val✝
h :
  (match some val✝ with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inl a
n : ℕ
IH : ↑s n = ↑(pure a) n
⊢ ↑s (Nat.succ n) = ↑(pure a) (Nat.succ n)
exact s.2 IH