α : Type u_1
β : Type ?u.16645
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ pure (get t h) ≤ pure (get s (_ : IsPure s))
α : Type u_1
β : Type ?u.16645
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ t ≤ s
rw [eq_pure h, eq_pure (h.mono st)]
α : Type u_1
β : Type ?u.16645
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ get t h = get s (_ : IsPure s)
α : Type u_1
β : Type ?u.16645
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ pure (get t h) ≤ pure (get s (_ : IsPure s))
simp
no goals
α : Type u_1
β : Type ?u.16645
s t : Semiquot α
h : IsPure t
st : s ≤ t
⊢ get t h = get s (_ : IsPure s)
exact h _ (get_mem _) _ (st <| get_mem _)