case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ bind s f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a'
⊢ b = b'
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ bind s f
⊢ b = b'
rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ bind s f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'
case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ bind s f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a'
⊢ b = b'
rw [← h1 a's] at ba'
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ bind s f
a' : α
a's : a' ∈ s
ba' : b' ∈ f a
⊢ b = b'
exact h2 ba'