α : Type u
β : Type v
γ : Type w
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t
α : Type u
β : Type v
γ : Type w
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a' ∈ t
rw [mem_unique ma h1]
no goals
α : Type u
β : Type v
γ : Type w
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ s
⊢ a ∈ t
exact h2
α : Type u
β : Type v
γ : Type w
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s
α : Type u
β : Type v
γ : Type w
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a' ∈ s
rw [mem_unique ma h2]
no goals
α : Type u
β : Type v
γ : Type w
s t : Computation α
a : α
h1 : a ∈ s
h2 : a ∈ t
a' : α
ma : a' ∈ t
⊢ a ∈ s
exact h1