α : Type u
β : Type v
γ : Type w
s s' : Computation α
⊢ (match ↑s 0 with
      | none => Sum.inr (tail s)
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = think s'
α : Type u
β : Type v
γ : Type w
s s' : Computation α
⊢ destruct s = Sum.inr s' → s = think s'
dsimp [destruct]
case none
α : Type u
β : Type v
γ : Type w
s s' : Computation α
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.inr s'
⊢ s = think s'

case some
α : Type u
β : Type v
γ : Type w
s s' : Computation α
x✝ : Option α
f0✝ : ↑s 0 = x✝
a' : α
f0 : ↑s 0 = some a'
h :
  (match some a' with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = think s'
α : Type u
β : Type v
γ : Type w
s s' : Computation α
⊢ (match ↑s 0 with
      | none => Sum.inr (tail s)
      | some a => Sum.inl a) =
      Sum.inr s' →
    s = think s'
induction' f0 : s.1 0 with a' <;> intro h
case none
α : Type u
β : Type v
γ : Type w
s s' : Computation α
x✝ : Option α
f0✝ : ↑s 0 = x✝
f0 : ↑s 0 = none
h' : tail s = s'
⊢ s = think s'
case none
α : Type u
β : Type v
γ : Type w
s s' : Computation α
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.inr s'
⊢ s = think s'
injection h with h'
case none
α : Type u
β : Type v
γ : Type w
s s' : Computation α
x✝ : Option α
f0✝ : ↑s 0 = x✝
f0 : ↑s 0 = none
h' : tail s = s'
⊢ s = think (tail s)
case none
α : Type u
β : Type v
γ : Type w
s s' : Computation α
x✝ : Option α
f0✝ : ↑s 0 = x✝
f0 : ↑s 0 = none
h' : tail s = s'
⊢ s = think s'
rw [← h']
case none.mk
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ { val := f, property := al } = think (tail { val := f, property := al })
case none
α : Type u
β : Type v
γ : Type w
s s' : Computation α
x✝ : Option α
f0✝ : ↑s 0 = x✝
f0 : ↑s 0 = none
h' : tail s = s'
⊢ s = think (tail s)
cases' s with f al
case none.mk.a
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ ↑{ val := f, property := al } = ↑(think (tail { val := f, property := al }))
case none.mk
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ { val := f, property := al } = think (tail { val := f, property := al })
apply Subtype.eq
case none.mk.a
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ f = Stream'.cons none (Stream'.tail f)
case none.mk.a
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ ↑{ val := f, property := al } = ↑(think (tail { val := f, property := al }))
dsimp [think, tail]
case none.mk.a
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ f = Stream'.cons (↑{ val := f, property := al } 0) (Stream'.tail f)
case none.mk.a
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ f = Stream'.cons none (Stream'.tail f)
rw [← f0]
no goals
case none.mk.a
α : Type u
β : Type v
γ : Type w
s' : Computation α
x✝ : Option α
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
f0✝ : ↑{ val := f, property := al } 0 = x✝
f0 : ↑{ val := f, property := al } 0 = none
h' : tail { val := f, property := al } = s'
⊢ f = Stream'.cons (↑{ val := f, property := al } 0) (Stream'.tail f)
exact (Stream'.eta f).symm
no goals
case some
α : Type u
β : Type v
γ : Type w
s s' : Computation α
x✝ : Option α
f0✝ : ↑s 0 = x✝
a' : α
f0 : ↑s 0 = some a'
h :
  (match some a' with
    | none => Sum.inr (tail s)
    | some a => Sum.inl a) =
    Sum.inr s'
⊢ s = think s'
contradiction